OAI/Analysis/JiangSu/Nonunital/CommonMinorant.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NonunitalGamma.hereditary_inr line 15
2. def OAI.NonunitalGamma.NormalizedTrace.rank line 28
3. lemma OAI.NonunitalGamma.NormalizedTrace.hereditary_rank_le line 31
4. lemma OAI.NonunitalGamma.NormalizedTrace.rank_cyclic line 36
5. lemma OAI.NonunitalGamma.exists_nonzero_cross line 41
6. theorem OAI.NonunitalGamma.exists_common_rank_minorant line 68
7. lemma OAI.NonunitalGamma.hereditary_mul_eq_zero line 87
8. lemma OAI.NonunitalGamma.exists_orthogonal_family_with_reserve line 103
9. lemma OAI.NonunitalGamma.exists_nonzero_positive line 145
10. lemma OAI.NonunitalGamma.exists_finite_common_rank_minorant line 149
11. theorem OAI.NonunitalGamma.small_hereditary_rank line 169