OAI/Analysis/CStarAlgebra/PureInfiniteness/IdealDetection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MainGap.compressedPositive line 14
2. lemma OAI.MainGap.compressedPositive_norm line 20
3. lemma OAI.MainGap.compressedPositive_square line 29
4. lemma OAI.MainGap.norm_one_sub_positive_contraction line 34
5. lemma OAI.MainGap.exists_rep_killing_ideal line 40
6. def OAI.MainGap.ScalarCuntzLE line 121
7. lemma OAI.MainGap.scalarCuntzLE_iff_finite line 124
8. lemma OAI.MainGap.ScalarCuntzLE.exists_approx line 147
9. lemma OAI.MainGap.ScalarCuntzLE.trans line 152
10. lemma OAI.MainGap.scalarCuntzLE_of_mem_Her line 157
11. lemma OAI.MainGap.scalarCuntzLE_of_order line 180
12. lemma OAI.MainGap.scalarCuntzLE_smul line 183