Complex number as a vector space over
This file contains three instances:
- any complex vector space is a real vector space;
- any finite dimensional complex vector space is a finite dimesional real vector space;
- the space of
ℝ-linear maps from a real vector space to a complex vector space is a complex vector space.
It also defines three linear maps:
They are bundled versions of the real part, the imaginary part, and the embedding of