OAI/Analysis/Commutator/MatrixCornerHilbert.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.MatrixCornerHilbert.fixedSpace line 19
2. lemma OAI.Kadison.MatrixCornerHilbert.mem_fixedSpace line 22
3. instance OAI.Kadison.MatrixCornerHilbert.(instance at line 26) line 26
4. instance OAI.Kadison.MatrixCornerHilbert.(instance at line 29) line 29
5. lemma OAI.Kadison.MatrixCornerHilbert.fixed_apply line 33
6. def OAI.Kadison.MatrixCornerHilbert.insert line 36
7. lemma OAI.Kadison.MatrixCornerHilbert.insert_apply line 45
8. def OAI.Kadison.MatrixCornerHilbert.matrixInsert line 55
9. lemma OAI.Kadison.MatrixCornerHilbert.adjoint_mem_fixed line 60
10. lemma OAI.Kadison.MatrixCornerHilbert.matrixInsert_orthogonal line 66
11. lemma OAI.Kadison.MatrixCornerHilbert.matrixInsert_adjoint line 77
12. lemma OAI.Kadison.MatrixCornerHilbert.matrixInsert_isHilbertSum line 90