OAI/Analysis/KadisonKastler/CommonReducingEquiv.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The same concrete subalgebra after faithful reducing restrictions

  1. theorem OAI.KadisonKastler.reducingAlgebra_mono line 18
  2. theorem OAI.KadisonKastler.commutantReducingHom_injective_of_inclusion line 26
  3. def OAI.KadisonKastler.reducingSubalgebraEquiv line 39
  4. theorem OAI.KadisonKastler.reducingSubalgebraEquiv_apply line 45
  5. theorem OAI.KadisonKastler.reducingSubalgebraEquiv_restrict line 49