# mathlibdocumentation

data.complex.module

# Complex number as a vector space over ℝ#

This file contains the following instances:

• Any •-structure (has_scalar, mul_action, distrib_mul_action, semimodule, algebra) on ℝ imbues a corresponding structure on ℂ. This includes the statement that ℂ is an ℝ algebra.
• any complex vector space is a real vector space;
• any finite dimensional complex vector space is a finite dimensional 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.re_lm;
• complex.im_lm;
• complex.of_real_lm;
• complex.conj_lm.

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

@[instance]
def complex.has_scalar {R : Type u_1} [ ] :
Equations
theorem complex.smul_re {R : Type u_1} [ ] (r : R) (z : ) :
(r z).re = r z.re
theorem complex.smul_im {R : Type u_1} [ ] (r : R) (z : ) :
(r z).im = r z.im
@[simp]
theorem complex.smul_coe {x : } {z : } :
x z = (x) * z
@[instance]
def complex.smul_comm_class {R : Type u_1} {S : Type u_2} [ ] [ ] [ ] :
@[instance]
def complex.is_scalar_tower {R : Type u_1} {S : Type u_2} [ S] [ ] [ ] [ ] :
@[instance]
def complex.mul_action {R : Type u_1} [monoid R] [ ] :
Equations
@[instance]
def complex.distrib_mul_action {R : Type u_1} [semiring R]  :
Equations
@[instance]
def complex.semimodule {R : Type u_1} [semiring R] [ ] :
Equations
@[instance]
def complex.algebra {R : Type u_1} [ ] :
Equations
@[simp]
@[instance]
@[simp]
@[simp]

fact version of the dimension of ℂ over ℝ, locally useful in the definition of the circle.

@[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 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] :
def complex.re_lm  :

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

Equations
@[simp]
def complex.im_lm  :

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

Equations
@[simp]

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

Equations
@[simp]
def complex.conj_lm  :

ℝ-linear map version of the complex conjugation function from ℂ to ℂ.

Equations
@[simp]