OAI/Analysis/KadisonKastler/CommonCyclicSubalgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The common subalgebra in the faithful cyclic representation

  1. def OAI.KadisonKastler.cyclicCommonHom line 18
  2. def OAI.KadisonKastler.cyclicCommonAlgebra line 22
  3. theorem OAI.KadisonKastler.cyclicCommonHom_injective line 25
  4. theorem OAI.KadisonKastler.cyclicCommonHom_normal line 31
  5. def OAI.KadisonKastler.cyclicCommonEquiv line 36
  6. theorem OAI.KadisonKastler.cyclicCommon_le line 41
  7. theorem OAI.KadisonKastler.cyclicCommon_restrict line 46
  8. theorem OAI.KadisonKastler.cyclicCommon_le_neighbor line 51
  9. theorem OAI.KadisonKastler.cyclicCommon_neighbor_restrict line 61