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.