OAI/Analysis/Commutator/HilbertFiniteMaps.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.HilbertFiniteMaps.Copies line 21
2. def OAI.Kadison.HilbertFiniteMaps.column line 23
3. lemma OAI.Kadison.HilbertFiniteMaps.column_apply line 28
4. lemma OAI.Kadison.HilbertFiniteMaps.adjoint_column_apply line 30
5. lemma OAI.Kadison.HilbertFiniteMaps.adjoint_column_comp line 36
6. lemma OAI.Kadison.HilbertFiniteMaps.column_norm_le_one line 41
7. def OAI.Kadison.HilbertFiniteMaps.amplify line 46
8. lemma OAI.Kadison.HilbertFiniteMaps.amplify_apply line 50
9. lemma OAI.Kadison.HilbertFiniteMaps.amplify_norm_le line 54
10. lemma OAI.Kadison.HilbertFiniteMaps.amplify_comp line 65
11. lemma OAI.Kadison.HilbertFiniteMaps.amplify_adjoint line 68
12. lemma OAI.Kadison.HilbertFiniteMaps.amplify_sub line 74