OAI/Analysis/KadisonKastler/WeightedStripCyclic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Identifying the weighted strip through cyclic spectral coordinates

  1. theorem OAI.KadisonKastler.weightedStripOperator_eq_group line 20