OAI/Analysis/Pureness/States/FiniteFamilyNormalizedMatrices.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.normalizedPositiveLevel line 14
2. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.normalizedPositiveLevel_unit line 17
3. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.normalizedPositiveLevel_metricSize_add line 24
4. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.normalizedPositiveLevel_sqrt_add line 29
5. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.normalizedPositiveLevel_scalar line 34
6. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.normalizedPositiveLevel_scalar_complex line 40
7. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.normalizedPositiveLevel_scalarCoefficient line 52