OAI/Analysis/KadisonKastler/StateBicentralizerAlgebra.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Algebra operations on the faithful state bicentralizer

  1. theorem OAI.KadisonKastler.stateBicentralizerMember_zero line 17
  2. theorem OAI.KadisonKastler.stateBicentralizerMember_one line 23
  3. theorem OAI.KadisonKastler.stateBicentralizerMember_add line 29
  4. theorem OAI.KadisonKastler.stateBicentralizerMember_smul line 41
  5. theorem OAI.KadisonKastler.stateBicentralizerMember_mul line 49
  6. def OAI.KadisonKastler.stateBicentralizerAlgebra line 62