OAI/Analysis/Pureness/Quasitrace/QuasitraceMatrixDiagonal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.PositiveQuasitrace.sum_commute line 14
2. lemma OAI.CuntzPureness.positiveQuasitrace_matrixCorner_eq line 30
3. lemma OAI.CuntzPureness.positiveQuasitrace_scalarMatrix line 48
4. lemma OAI.CuntzPureness.matrixInclusion_scalar_one line 66
5. lemma OAI.CuntzPureness.finiteSpectralPositiveQuasitrace_scalarMatrix line 94