OAI/Analysis/Commutator/HilbertBiprodProjections.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.HilbertBiprod.left line 19
2. abbrev OAI.Kadison.HilbertBiprod.right line 21
3. lemma OAI.Kadison.HilbertBiprod.left_projection line 23
4. lemma OAI.Kadison.HilbertBiprod.right_projection line 30
5. lemma OAI.Kadison.HilbertBiprod.left_add_right line 38
6. lemma OAI.Kadison.HilbertBiprod.left_mul_right line 43
7. lemma OAI.Kadison.HilbertBiprod.left_commutes line 48
8. lemma OAI.Kadison.HilbertBiprod.right_commutes line 54
9. lemma OAI.Kadison.HilbertBiprod.adjoint_inlL line 59
10. lemma OAI.Kadison.HilbertBiprod.adjoint_inrL line 67
11. lemma OAI.Kadison.HilbertBiprod.inl_adjoint line 75
12. lemma OAI.Kadison.HilbertBiprod.inr_adjoint line 81
13. lemma OAI.Kadison.HilbertBiprod.right_ne_zero line 88