OAI/Analysis/KadisonKastler/TwoStateModularIdentification.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Identifying both diagonal modular actions with their original states

  1. theorem OAI.KadisonKastler.twoStateVectorAt_cyclic line 23
  2. theorem OAI.KadisonKastler.twoStateVectorAt_separating line 31
  3. def OAI.KadisonKastler.twoStateConstructedResolution line 37
  4. def OAI.KadisonKastler.twoStateCornerResolution line 47
  5. theorem OAI.KadisonKastler.twoStateCornerAction_identification line 56