OAI/Analysis/Pureness/Comparison/MatrixDiagonal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzComparison.matrixDiagonalHom line 16
2. lemma OAI.CuntzComparison.matrixDiagonal_apply line 26
3. lemma OAI.CuntzComparison.matrixDiagonal_nonneg line 29
4. lemma OAI.CuntzComparison.matrixDiagonal_cfc line 39
5. lemma OAI.CuntzComparison.TracialState.matrixTrace_diagonal line 54
6. lemma OAI.CuntzComparison.TracialState.normalizedMatrixTrace_scale line 58
7. theorem OAI.CuntzComparison.TracialState.matrixSupportMass_diagonal line 67