Metamath Proof Explorer

Table of Contents - 19.6.3. Operations on Hilbert space operators

1. hoaddcl
2. homulcl
3. hoeq
4. hoeqi
5. hoscli
6. hodcli
7. hocoi
8. hococli
9. hocofi
10. hocofni
11. hoaddcli
12. hosubcli
13. hoaddfni
14. hosubfni
15. hoaddcomi
16. hosubcl
17. hoaddcom
18. hodsi
19. hoaddassi
20. hoadd12i
21. hoadd32i
22. hocadddiri
23. hocsubdiri
24. ho2coi
25. hoaddass
26. hoadd32
27. hoadd4
28. hocsubdir
29. hoaddid1i
30. hodidi
31. ho0coi
32. hoid1i
33. hoid1ri
34. hoaddid1
35. hodid
36. hon0
37. hodseqi
38. ho0subi
39. honegsubi
40. ho0sub
41. hosubid1
42. honegsub
43. homulid2
44. homco1
45. homulass
46. hoadddi
47. hoadddir
48. homul12
49. honegneg
50. hosubneg
51. hosubdi
52. honegdi
53. honegsubdi
54. honegsubdi2
55. hosubsub2
56. hosub4
57. hosubadd4
58. hoaddsubass
59. hoaddsub
60. hosubsub
61. hosubsub4
62. ho2times
63. hoaddsubassi
64. hoaddsubi
65. hosd1i
66. hosd2i
67. hopncani
68. honpcani
69. hosubeq0i
70. honpncani
71. ho01i
72. ho02i
73. hoeq1
74. hoeq2
75. adjmo
76. adjsym
77. eigrei
78. eigre
79. eigposi
80. eigorthi
81. eigorth