OAI/Analysis/Pureness/States/FiniteFamilyScalarUltraproduct.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.normalizedScalarPositive line 16
2. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.scalarCoefficientAWMap line 30
3. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.scalarCoefficientAWMap_commute line 36
4. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.scalarCoefficientAWMap_eq line 42
5. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.scalarTracialMatrixAWEmbedding line 64
6. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.scalarTracialMatrixAWEmbedding_map line 71
7. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.scalarTracialMatrixAWEmbedding_injective line 77
8. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.scalarTracialMatrixAWEmbedding_isometry line 85
9. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.scalarTracialMatrixAWEmbedding_commute line 90