OAI/Analysis/CStarAlgebra/PureInfiniteness/IdealComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MainGap.ScalarCuntzLE.conjugate_scalar line 15
2. lemma OAI.MainGap.scalarCuntzLE_left_square line 24
3. lemma OAI.MainGap.scalarCuntzLE_add_of_proper line 36
4. lemma OAI.MainGap.square_add_le line 59
5. lemma OAI.MainGap.square_comparison_add line 69
6. lemma OAI.MainGap.idealSpan_square_comparison line 76
7. theorem OAI.MainGap.closedIdeal_comparison line 94
8. lemma OAI.MainGap.scalarCuntzLE_of_inr line 117