OAI/Analysis/Pureness/Cuntz/MatrixTraces.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.positive_square_factor line 9
2. def OAI.CuntzPureness.matrixTraceLinear line 13
3. lemma OAI.CuntzPureness.matrixTraceLinear_apply line 19
4. lemma OAI.CuntzPureness.matrix_entry_nonneg line 22
5. def OAI.CuntzPureness.matrixTrace line 29
6. lemma OAI.CuntzPureness.matrixTrace_apply line 39
7. lemma OAI.CuntzPureness.matrixTrace_one line 42
8. lemma OAI.CuntzPureness.matrixTrace_tracial line 46
9. def OAI.CuntzPureness.matrixTracialState line 56
10. def OAI.CuntzPureness.matrixRank line 73