OAI/Analysis/KadisonKastler/TracialConstantEmbedding.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The constant algebra inside its tracial sequence quotient

  1. def OAI.KadisonKastler.boundedToVarying line 16
  2. theorem OAI.KadisonKastler.boundedToVarying_surjective line 25
  3. def OAI.KadisonKastler.constantVarying line 32
  4. def OAI.KadisonKastler.tracialConstantEmbedding line 41
  5. theorem OAI.KadisonKastler.tracialConstantEmbedding_injective line 45
  6. theorem OAI.KadisonKastler.tracialConstantQuotient_infinite line 54