OAI/Analysis/JiangSu/Comparison/CompletedRankComparison.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Pureness.completedRankRealModule line 18
2. abbrev OAI.Pureness.completedRankRealSMulZero line 21
3. abbrev OAI.Pureness.completedRankRealAlgebra line 24
4. lemma OAI.Pureness.completed_sqrt_row_hereditary line 27
5. lemma OAI.Pureness.completed_sqrt_row_weight line 41
6. lemma OAI.Pureness.completedWeight_le_rank_of_unitized_cuntz line 59
7. theorem OAI.Pureness.completedRootRank_le_of_unitized_cuntz line 92
8. lemma OAI.Pureness.normalizedRoot_mul_sqrt_of_le_tendsto line 115
9. theorem OAI.Pureness.cuntzSubequiv_of_nonneg_of_le line 155
10. lemma OAI.Pureness.rank_mono_positive line 167