OAI/Analysis/Pureness/Comparison/MatrixTrace.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzComparison.matrixRealCFC line 10
2. instance OAI.CuntzComparison.matrixRealNonUnitalCFC line 13
3. instance OAI.CuntzComparison.matrixRealNonnegSpectrum line 17
4. def OAI.CuntzComparison.TracialState.matrixTraceLinear line 20
5. lemma OAI.CuntzComparison.TracialState.matrixTrace_one line 26
6. lemma OAI.CuntzComparison.TracialState.matrixTrace_cyclic line 31
7. lemma OAI.CuntzComparison.TracialState.matrixTrace_nonneg line 42
8. def OAI.CuntzComparison.TracialState.matrixTracePositive line 52
9. def OAI.CuntzComparison.TracialState.normalizedMatrixTrace line 61
10. def OAI.CuntzComparison.TracialState.matrixSupportMass line 75