OAI/Analysis/KadisonKastler/MinimalProjectionEquivalence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Minimal projections, equivalence and automorphisms in a factor

  1. theorem OAI.KadisonKastler.partialIsometry_target_ne_zero line 18
  2. theorem OAI.KadisonKastler.minimalProjection_partialIsometry_target line 28
  3. theorem OAI.KadisonKastler.minimalProjection_map line 67
  4. theorem OAI.KadisonKastler.factor_scalar_algebra line 87
  5. theorem OAI.KadisonKastler.factor_exists_minimal_below line 95
  6. theorem OAI.KadisonKastler.factor_minimal_projections_equivalent line 105