Complex number as a vector space over ℝ
This file contains three instances:
ℂis anℝalgebra;- any complex vector space is a 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 ℝ in ℂ,
as ℝ-linear maps.
@[instance]
Equations
@[instance]
Equations
@[instance]
def
linear_map.module
(E : Type u_1)
[add_comm_group E]
[module ℝ E]
(F : Type u_2)
[add_comm_group F]
[module ℂ F] :
Equations
Linear map version of the canonical embedding of ℝ in ℂ.
Equations
- complex.linear_map.of_real = {to_fun := coe coe_to_lift, map_add' := complex.linear_map.of_real._proof_1, map_smul' := complex.linear_map.of_real._proof_2}