OAI/Analysis/KadisonKastler/StateCoreTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Cores of state-preserving cyclic representations

The modular groups give spatially isomorphic concrete cores.

  1. theorem OAI.KadisonKastler.statePreservingUnitary_algebra line 23
  2. theorem OAI.KadisonKastler.constructedCore_equiv_of_statePreserving line 45