OAI/Analysis/KadisonSimilarity/Tracial/InternalSourceStages.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The generating matrix stages, viewed internally in their generated von Neumann algebra. This retains the actual operators and matrix sizes.

  1. def OAI.KadisonSimilarity.generatedInternalStage line 16
  2. theorem OAI.KadisonSimilarity.generatedInternalStage_size line 45
  3. theorem OAI.KadisonSimilarity.generatedInternalStage_sizes_cofinal line 48