OAI/Analysis/Commutator/KaplanskyFull.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.Kaplansky.offDiagonal line 23
2. lemma OAI.Kadison.Kaplansky.offDiagonal_zero line 27
3. lemma OAI.Kadison.Kaplansky.offDiagonal_one line 31
4. lemma OAI.Kadison.Kaplansky.offDiagonal_selfAdjoint line 35
5. lemma OAI.Kadison.Kaplansky.offDiagonal_norm_le line 43
6. lemma OAI.Kadison.Kaplansky.entry_offDiagonal line 54
7. lemma OAI.Kadison.Kaplansky.star_bicommutant line 60
8. lemma OAI.Kadison.Kaplansky.offDiagonal_bicommutant line 73
9. lemma OAI.Kadison.Kaplansky.single_norm line 88
10. lemma OAI.Kadison.Kaplansky.entry_norm_le line 94
11. theorem OAI.Kadison.Kaplansky.contraction_finite_approx line 105