mathlib documentation

data.complex.module

Complex number as a vector space over #

This file contains the following instances:

It also defines bundled versions of four standard maps (respectively, the real part, the imaginary part, the embedding of in , and the complex conjugate):

It also provides a universal property of the complex numbers complex.lift, which constructs a ℂ →ₐ[ℝ] A into any -algebra A given a square root of -1.

@[protected, instance]
def complex.has_smul {R : Type u_1} [has_smul R ] :
Equations
theorem complex.smul_re {R : Type u_1} [has_smul R ] (r : R) (z : ) :
(r z).re = r z.re
theorem complex.smul_im {R : Type u_1} [has_smul R ] (r : R) (z : ) :
(r z).im = r z.im
@[simp]
theorem complex.real_smul {x : } {z : } :
x z = x * z
@[protected, instance]
def complex.smul_comm_class {R : Type u_1} {S : Type u_2} [has_smul R ] [has_smul S ] [smul_comm_class R S ] :
@[protected, instance]
def complex.is_scalar_tower {R : Type u_1} {S : Type u_2} [has_smul R S] [has_smul R ] [has_smul S ] [is_scalar_tower R S ] :
@[protected, instance]
@[protected, instance]
def complex.mul_action {R : Type u_1} [monoid R] [mul_action R ] :
Equations
@[protected, instance]
def complex.algebra {R : Type u_1} [comm_semiring R] [algebra R ] :
Equations
@[protected, instance]
@[simp]
theorem alg_hom.map_coe_real_complex {A : Type u_3} [semiring A] [algebra A] (f : →ₐ[] A) (x : ) :

We need this lemma since complex.coe_algebra_map diverts the simp-normal form away from alg_hom.commutes.

@[ext]
theorem complex.alg_hom_ext {A : Type u_3} [semiring A] [algebra A] ⦃f g : →ₐ[] A⦄ (h : f complex.I = g complex.I) :
f = g

Two -algebra homomorphisms from ℂ are equal if they agree on complex.I.

@[protected]
noncomputable def complex.basis_one_I  :

has a basis over given by 1 and I.

Equations
@[simp]

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

@[protected, instance]
def module.complex_to_real (E : Type u_1) [add_comm_group E] [module E] :
Equations
@[protected, instance]
@[simp, norm_cast]
theorem complex.coe_smul {E : Type u_1} [add_comm_group E] [module E] (x : ) (y : E) :
x y = x y
theorem dim_real_of_complex (E : Type u_1) [add_comm_group E] [module E] :
@[protected, instance]

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

Equations

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

Equations

-algebra morphism version of the canonical embedding of in .

Equations

-algebra isomorphism version of the complex conjugation function from to

Equations
@[simp]

The matrix representation of conj_ae.

The identity and the complex conjugation are the only two -algebra homomorphisms of .

def complex.lift_aux {A : Type u_1} [ring A] [algebra A] (I' : A) (hf : I' * I' = -1) :

There is an alg_hom from to any -algebra with an element that squares to -1.

See complex.lift for this as an equiv.

Equations
@[simp]
theorem complex.lift_aux_apply {A : Type u_1} [ring A] [algebra A] (I' : A) (hI' : I' * I' = -1) (z : ) :
theorem complex.lift_aux_apply_I {A : Type u_1} [ring A] [algebra A] (I' : A) (hI' : I' * I' = -1) :
def complex.lift {A : Type u_1} [ring A] [algebra A] :
{I' // I' * I' = -1} ( →ₐ[] A)

A universal property of the complex numbers, providing a unique ℂ →ₐ[ℝ] A for every element of A which squares to -1.

This can be used to embed the complex numbers in the quaternions.

This isomorphism is named to match the very similar zsqrtd.lift.

Equations
@[simp]
theorem complex.lift_apply {A : Type u_1} [ring A] [algebra A] (I' : {I' // I' * I' = -1}) :
@[simp]
theorem complex.lift_symm_apply_coe {A : Type u_1} [ring A] [algebra A] (F : →ₐ[] A) :