# mathlibdocumentation

data.complex.module

# 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:

• complex.linear_map.re;
• complex.linear_map.im;
• complex.linear_map.of_real.

They are bundled versions of the real part, the imaginary part, and the embedding of ℝ in ℂ, as ℝ-linear maps.

@[instance]

Equations
@[simp]

@[simp]
theorem complex.re_smul (a : ) (z : ) :
(a z).re = a * z.re

@[simp]
theorem complex.im_smul (a : ) (z : ) :
(a z).im = a * z.im

@[instance]

@[simp]

@[simp]

@[instance]
def module.complex_to_real (E : Type u_1) [ E] :
E

Equations
@[instance]
def module.real_complex_tower (E : Type u_1) [ E] :

@[instance]
def linear_map.module (E : Type u_1) [ E] (F : Type u_2) [ F] :

Equations
@[instance]
def finite_dimensional.complex_to_real (E : Type u_1) [ E]  :

theorem dim_real_of_complex (E : Type u_1) [ E] :
=

theorem findim_real_of_complex (E : Type u_1) [ E] :

Linear map version of the real part function, from ℂ to ℝ.

Equations
@[simp]

Linear map version of the imaginary part function, from ℂ to ℝ.

Equations
@[simp]

Linear map version of the canonical embedding of ℝ in ℂ.

Equations
@[simp]