OAI/Analysis/Pureness/Comparison/MatrixExtendedTrace.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzComparison.compression_starMul_stage line 12
2. lemma OAI.CuntzComparison.compression_mulStar_stage line 20
3. lemma OAI.CuntzComparison.TracialState.matrixTraceValue_compression_tracial line 29
4. lemma OAI.CuntzComparison.TracialState.matrixTraceValue_compression_eq_corner line 35
5. lemma OAI.CuntzComparison.TracialState.matrixTraceValue_compression_bound line 40
6. lemma OAI.CuntzComparison.TracialState.matrixTraceValue_tracial_le line 48
7. theorem OAI.CuntzComparison.TracialState.matrixTraceValue_tracial line 65
8. def OAI.CuntzComparison.TracialState.matrixExtendedTrace line 73
9. theorem OAI.CuntzComparison.TracialState.matrixExtendedTrace_stage line 81
10. theorem OAI.CuntzComparison.TracialState.matrixExtendedTrace_pullback line 85
11. theorem OAI.CuntzComparison.TracialState.matrixExtendedTrace_rank_stage line 90