OAI/Analysis/Pureness/States/ScalarMatrixUltraEmbedding.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.normalizedMatrixState_scalarPositive line 13
2. abbrev OAI.CuntzPureness.ScalarTracialMatrixUltraproduct line 25
3. lemma OAI.CuntzPureness.scalarCoefficientAWMap_eq line 31
4. def OAI.CuntzPureness.scalarTracialMatrixAWEmbedding line 53
5. lemma OAI.CuntzPureness.scalarTracialMatrixAWEmbedding_map line 60
6. lemma OAI.CuntzPureness.scalarTracialMatrixAWEmbedding_injective line 66
7. lemma OAI.CuntzPureness.scalarTracialMatrixAWEmbedding_isometry line 74
8. lemma OAI.CuntzPureness.scalarTracialMatrixAWEmbedding_commute line 79