OAI/Analysis/KadisonKastler/FactorSpatialSplit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Spatial splitting for factors with countably decomposable commutant

  1. theorem OAI.KadisonKastler.scalarCenter_commutant line 16
  2. theorem OAI.KadisonKastler.exists_selfAdjoint_split_of_factor_commutant line 24
  3. theorem OAI.KadisonKastler.exists_selfAdjoint_split_of_factor line 56