mathlib documentation

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:

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

@[instance]

def complex.algebra_over_reals :

algebra ℝ ℂ

Equations

complex.algebra_over_reals = complex.of_real.to_algebra

@[simp]

theorem complex.coe_algebra_map :

⇑(algebra_map ℝ ℂ) = ⇑complex.of_real

@[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

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

@[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 linear_map.module (E : Type u_1) [add_comm_group E] [module ℝ E] (F : Type u_2) [add_comm_group F] [module ℂ F] :

module ℂ (E →ₗ[ℝ ] F)

Equations

linear_map.module E F = linear_map.module_extend_scalars ℝ ℂ E F

@[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.linear_map.re :

ℂ →ₗ[ℝ ] ℝ

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}

@[simp]

theorem complex.linear_map.coe_re :

⇑complex.linear_map.re = complex.re

def complex.linear_map.im :

ℂ →ₗ[ℝ ] ℝ

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}

@[simp]

theorem complex.linear_map.coe_im :

⇑complex.linear_map.im = complex.im

def complex.linear_map.of_real :

ℝ →ₗ[ℝ ] ℂ

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}

@[simp]

theorem complex.linear_map.coe_of_real :

⇑complex.linear_map.of_real = coe