Metamath Proof Explorer


Table of Contents - 12.5.2. Subcomplex vector spaces

Usually, "complex vector spaces" are vector spaces over the field of the complex numbers, see for example the definition in [Roman] p. 36.

In the setting of set.mm, it is convenient to consider collectively vector spaces on subfields of the field of complex numbers. We call these, "subcomplex vector spaces" and collect them in the class defined in df-cvs and characterized in iscvs. These include rational vector spaces (qcvs), real vector spaces (recvs) and complex vector spaces (cncvs).

This definition is analogous to the definition of subcomplex modules (and their class ), which are modules over subrings of the field of complex numbers. Note that ZZ-modules (that are roughly the same thing as Abelian groups, see zlmclm) are subcomplex modules but are not subcomplex vector spaces (see zclmncvs), because the ring ZZ is not a division ring (see zringndrg).

Since the field of complex numbers is commutative, so are its subrings, so there is no need to explicitly state "left module" or "left vector space" for subcomplex modules or vector spaces.

  1. ccvs
  2. df-cvs
  3. cvslvec
  4. cvsclm
  5. iscvs
  6. iscvsp
  7. iscvsi
  8. cvsi
  9. cvsunit
  10. cvsdiv
  11. cvsdivcl
  12. cvsmuleqdivd
  13. cvsdiveqd
  14. cnlmodlem1
  15. cnlmodlem2
  16. cnlmodlem3
  17. cnlmod4
  18. cnlmod
  19. cnstrcvs
  20. cnrbas
  21. cnrlmod
  22. cnrlvec
  23. cncvs
  24. recvs
  25. recvsOLD
  26. qcvs
  27. zclmncvs