mathlib documentation

data.complex.module

Complex number as a vector space over #

This file contains the following instances:

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 ] :
Equations
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 ] :
@[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 ] :

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

@[instance]

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

Equations

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

Equations

Linear map version of the canonical embedding of in .

Equations

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

Equations