Metamath Proof Explorer

Table of Contents - 18.7.2. Standard axioms for a complex Hilbert space

  1. hlex
  2. hladdf
  3. hlcom
  4. hlass
  5. hl0cl
  6. hladdid
  7. hlmulf
  8. hlmulid
  9. hlmulass
  10. hldi
  11. hldir
  12. hlmul0
  13. hlipf
  14. hlipcj
  15. hlipdir
  16. hlipass
  17. hlipgt0
  18. hlcompl