Complex number as a vector space over ℝ
This file contains three instances:
ℂ
is anℝ
algebra;- 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 ℝ
in ℂ
,
as ℝ
-linear maps.
@[instance]
Equations
@[instance]
Equations
@[instance]
@[instance]
def
finite_dimensional.complex_to_real
(E : Type u_1)
[add_comm_group E]
[module ℂ E]
[finite_dimensional ℂ E] :
theorem
dim_real_of_complex
(E : Type u_1)
[add_comm_group E]
[module ℂ E] :
vector_space.dim ℝ E = 2 * vector_space.dim ℂ E
Linear map version of the real part function, from ℂ
to ℝ
.
Equations
- complex.linear_map.re = {to_fun := λ (x : ℂ), x.re, map_add' := complex.add_re, map_smul' := complex.re_smul}
Linear map version of the imaginary part function, from ℂ
to ℝ
.
Equations
- complex.linear_map.im = {to_fun := λ (x : ℂ), x.im, map_add' := complex.add_im, map_smul' := complex.im_smul}
Linear map version of the canonical embedding of ℝ
in ℂ
.
Equations
- complex.linear_map.of_real = {to_fun := coe coe_to_lift, map_add' := complex.of_real_add, map_smul' := complex.linear_map.of_real._proof_1}