mathlib documentation

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:

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} [has_scalar R ℝ] :

has_scalar R ℂ

Equations

complex.has_scalar = {smul := λ (r : R) (x : ℂ), {re := r • x.re - 0 * x.im, im := r • x.im + 0 * x.re}}

theorem complex.smul_re {R : Type u_1} [has_scalar R ℝ] (r : R) (z : ℂ) :

(r • z).re = r • z.re

theorem complex.smul_im {R : Type u_1} [has_scalar R ℝ] (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} [has_scalar R ℝ] [has_scalar S ℝ] [smul_comm_class R S ℝ] :

smul_comm_class R S ℂ

@[instance]

def complex.is_scalar_tower {R : Type u_1} {S : Type u_2} [has_scalar R S] [has_scalar R ℝ] [has_scalar S ℝ] [is_scalar_tower R S ℝ] :

is_scalar_tower R S ℂ

@[instance]

def complex.mul_action {R : Type u_1} [monoid R] [mul_action R ℝ] :

mul_action R ℂ

Equations

complex.mul_action = {to_has_scalar := complex.has_scalar mul_action.to_has_scalar, one_smul := _, mul_smul := _}

@[instance]

def complex.distrib_mul_action {R : Type u_1} [semiring R] [distrib_mul_action R ℝ] :

distrib_mul_action R ℂ

Equations

complex.distrib_mul_action = {to_mul_action := complex.mul_action distrib_mul_action.to_mul_action, smul_add := _, smul_zero := _}

@[instance]

def complex.semimodule {R : Type u_1} [semiring R] [semimodule R ℝ] :

semimodule R ℂ

Equations

complex.semimodule = {to_distrib_mul_action := complex.distrib_mul_action semimodule.to_distrib_mul_action, add_smul := _, zero_smul := _}

@[instance]

def complex.algebra {R : Type u_1} [comm_semiring R] [algebra R ℝ] :

Equations

complex.algebra = {to_has_scalar := {smul := has_scalar.smul complex.has_scalar}, to_ring_hom := {to_fun := (complex.of_real.comp (algebra_map R ℝ)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

theorem complex.complex_ordered_semimodule :

ordered_semimodule ℝ ℂ

@[simp]

theorem complex.coe_algebra_map :

⇑(algebra_map ℝ ℂ) = ⇑complex.of_real

theorem complex.is_basis_one_I :

is_basis ℝ ![1, complex.I]

@[instance]

def complex.finite_dimensional :

finite_dimensional ℝ ℂ

@[simp]

theorem complex.findim_real_complex :

finite_dimensional.findim ℝ ℂ = 2

@[simp]

theorem complex.dim_real_complex :

vector_space.dim ℝ ℂ = 2

theorem complex.dim_real_complex' :

(vector_space.dim ℝ ℂ).lift = 2

theorem complex.findim_real_complex_fact :

fact (finite_dimensional.findim ℝ ℂ = 2)

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) [add_comm_group E] [module ℂ E] :

Equations

module.complex_to_real E = restrict_scalars.semimodule ℝ ℂ E

@[instance]

def module.real_complex_tower (E : Type u_1) [add_comm_group E] [module ℂ E] :

is_scalar_tower ℝ ℂ E

@[instance]

def finite_dimensional.complex_to_real (E : Type u_1) [add_comm_group E] [module ℂ E] [finite_dimensional ℂ 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

theorem findim_real_of_complex (E : Type u_1) [add_comm_group E] [module ℂ E] :

finite_dimensional.findim ℝ E = 2 * finite_dimensional.findim ℂ E

def complex.re_lm :

ℂ →ₗ[ℝ ] ℝ

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

Equations

complex.re_lm = {to_fun := λ (x : ℂ), x.re, map_add' := complex.add_re, map_smul' := complex.re_lm._proof_1}

@[simp]

theorem complex.re_lm_coe :

⇑complex.re_lm = complex.re

def complex.im_lm :

ℂ →ₗ[ℝ ] ℝ

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

Equations

complex.im_lm = {to_fun := λ (x : ℂ), x.im, map_add' := complex.add_im, map_smul' := complex.im_lm._proof_1}

@[simp]

theorem complex.im_lm_coe :

⇑complex.im_lm = complex.im

def complex.of_real_lm :

ℝ →ₗ[ℝ ] ℂ

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

Equations

complex.of_real_lm = {to_fun := coe coe_to_lift, map_add' := complex.of_real_add, map_smul' := complex.of_real_lm._proof_1}

@[simp]

theorem complex.of_real_lm_coe :

⇑complex.of_real_lm = coe

def complex.conj_lm :

ℂ →ₗ[ℝ ] ℂ

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

Equations

complex.conj_lm = {to_fun := complex.conj.to_fun, map_add' := complex.conj_lm._proof_1, map_smul' := complex.conj_lm._proof_2}

@[simp]

theorem complex.conj_lm_coe :

⇑complex.conj_lm = ⇑complex.conj