OAI/Analysis/Commutator/HilbertPair.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.HilbertPair.Space line 18
2. def OAI.Kadison.HilbertPair.left line 20
3. def OAI.Kadison.HilbertPair.right line 30
4. lemma OAI.Kadison.HilbertPair.left_apply line 41
5. lemma OAI.Kadison.HilbertPair.right_apply line 44
6. lemma OAI.Kadison.HilbertPair.left_adjoint line 46
7. lemma OAI.Kadison.HilbertPair.right_adjoint line 52
8. lemma OAI.Kadison.HilbertPair.left_adjoint_left line 58
9. lemma OAI.Kadison.HilbertPair.right_adjoint_right line 64
10. lemma OAI.Kadison.HilbertPair.left_adjoint_right line 70
11. lemma OAI.Kadison.HilbertPair.right_adjoint_left line 76