OAI/Analysis/JiangSu/Nonunital/MatrixComparison.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NonunitalGamma.sqrt_conjugate line 18
2. lemma OAI.NonunitalGamma.NormalizedTrace.continuous_unitized_eval line 24
3. lemma OAI.NonunitalGamma.NormalizedTrace.continuous_matrix_eval line 29
4. def OAI.NonunitalGamma.scalarOne line 36
5. def OAI.NonunitalGamma.scalarCorner line 47
6. lemma OAI.NonunitalGamma.inr_scalarCorner line 50
7. lemma OAI.NonunitalGamma.scalarCorner_injective line 66
8. lemma OAI.NonunitalGamma.NormalizedTrace.matrix_rank_inr line 72
9. lemma OAI.NonunitalGamma.trace_lt_rank line 84
10. lemma OAI.NonunitalGamma.matrix_comparison_inr line 103
11. lemma OAI.NonunitalGamma.hereditary_inr_reflect line 145
12. lemma OAI.NonunitalGamma.uniform_positive_trace line 172
13. lemma OAI.NonunitalGamma.rank_approximant_below_trace line 181
14. theorem OAI.NonunitalGamma.almost_projection line 218