mathlib docs: data.complex.basic

source

structure complex :

Type

re : ℝ
im : ℝ

Complex numbers consist of two reals: a real part re and an imaginary part im.

source

@[instance]

def complex.decidable_eq :

decidable_eq ℂ

Equations

complex.decidable_eq = classical.dec_eq ℂ

source

def complex.equiv_real_prod :

ℂ ≃ ℝ × ℝ

The equivalence between the complex numbers and ℝ × ℝ.

Equations

complex.equiv_real_prod = {to_fun := λ (z : ℂ), (z.re, z.im), inv_fun := λ (p : ℝ × ℝ), {re := p.fst, im := p.snd}, left_inv := complex.equiv_real_prod._proof_1, right_inv := complex.equiv_real_prod._proof_2}

source

@[simp]

theorem complex.equiv_real_prod_apply (z : ℂ) :

⇑complex.equiv_real_prod z = (z.re, z.im)

source

theorem complex.equiv_real_prod_symm_re (x y : ℝ) :

(⇑(complex.equiv_real_prod.symm) (x, y)).re = x

source

theorem complex.equiv_real_prod_symm_im (x y : ℝ) :

(⇑(complex.equiv_real_prod.symm) (x, y)).im = y

source

@[simp]

theorem complex.eta (z : ℂ) :

{re := z.re, im := z.im} = z

source

@[ext]

theorem complex.ext {z w : ℂ} :

z.re = w.re → z.im = w.im → z = w

source

theorem complex.ext_iff {z w : ℂ} :

z = w ↔ z.re = w.re ∧ z.im = w.im

source

@[instance]

def complex.has_coe :

has_coe ℝ ℂ

Equations

complex.has_coe = {coe := λ (r : ℝ), {re := r, im := 0}}

source

@[simp]

theorem complex.of_real_re (r : ℝ) :

↑r.re = r

source

@[simp]

theorem complex.of_real_im (r : ℝ) :

↑r.im = 0

source

@[simp]

theorem complex.of_real_inj {z w : ℝ} :

↑z = ↑w ↔ z = w

source

@[instance]

def complex.has_zero :

has_zero ℂ

Equations

complex.has_zero = {zero := ↑0}

source

@[instance]

def complex.inhabited :

inhabited ℂ

Equations

complex.inhabited = {default := 0}

source

@[simp]

theorem complex.zero_re :

0.re = 0

source

@[simp]

theorem complex.zero_im :

0.im = 0

source

@[simp]

theorem complex.of_real_zero :

↑0 = 0

source

@[simp]

theorem complex.of_real_eq_zero {z : ℝ} :

↑z = 0 ↔ z = 0

source

theorem complex.of_real_ne_zero {z : ℝ} :

↑z ≠ 0 ↔ z ≠ 0

source

@[instance]

def complex.has_one :

has_one ℂ

Equations

complex.has_one = {one := ↑1}

source

@[simp]

theorem complex.one_re :

1.re = 1

source

@[simp]

theorem complex.one_im :

1.im = 0

source

@[simp]

theorem complex.of_real_one :

↑1 = 1

source

@[instance]

def complex.has_add :

has_add ℂ

Equations

complex.has_add = {add := λ (z w : ℂ), {re := z.re + w.re, im := z.im + w.im}}

source

@[simp]

theorem complex.add_re (z w : ℂ) :

(z + w).re = z.re + w.re

source

@[simp]

theorem complex.add_im (z w : ℂ) :

(z + w).im = z.im + w.im

source

@[simp]

theorem complex.bit0_re (z : ℂ) :

(bit0 z).re = bit0 z.re

source

@[simp]

theorem complex.bit1_re (z : ℂ) :

(bit1 z).re = bit1 z.re

source

@[simp]

theorem complex.bit0_im (z : ℂ) :

(bit0 z).im = bit0 z.im

source

@[simp]

theorem complex.bit1_im (z : ℂ) :

(bit1 z).im = bit0 z.im

source

@[simp]

theorem complex.of_real_add (r s : ℝ) :

↑(r + s) = ↑r + ↑s

source

@[simp]

theorem complex.of_real_bit0 (r : ℝ) :

↑(bit0 r) = bit0 ↑r

source

@[simp]

theorem complex.of_real_bit1 (r : ℝ) :

↑(bit1 r) = bit1 ↑r

source

@[instance]

def complex.has_neg :

has_neg ℂ

Equations

complex.has_neg = {neg := λ (z : ℂ), {re := -z.re, im := -z.im}}

source

@[simp]

theorem complex.neg_re (z : ℂ) :

(-z).re = -z.re

source

@[simp]

theorem complex.neg_im (z : ℂ) :

(-z).im = -z.im

source

@[simp]

theorem complex.of_real_neg (r : ℝ) :

↑-r = -↑r

source

@[instance]

def complex.has_mul :

has_mul ℂ

Equations

complex.has_mul = {mul := λ (z w : ℂ), {re := z.re * w.re - z.im * w.im, im := z.re * w.im + z.im * w.re}}

source

@[simp]

theorem complex.mul_re (z w : ℂ) :

(z * w).re = z.re * w.re - z.im * w.im

source

@[simp]

theorem complex.mul_im (z w : ℂ) :

(z * w).im = z.re * w.im + z.im * w.re

source

@[simp]

theorem complex.of_real_mul (r s : ℝ) :

↑(r * s) = ↑r * ↑s

source

theorem complex.smul_re (r : ℝ) (z : ℂ) :

(↑r * z).re = r * z.re

source

theorem complex.smul_im (r : ℝ) (z : ℂ) :

(↑r * z).im = r * z.im

source

theorem complex.of_real_smul (r : ℝ) (z : ℂ) :

↑r * z = {re := r * z.re, im := r * z.im}

source

def complex.I :

ℂ

The imaginary unit.

Equations

complex.I = {re := 0, im := 1}

source

@[simp]

theorem complex.I_re :

complex.I.re = 0

source

@[simp]

theorem complex.I_im :

complex.I.im = 1

source

@[simp]

theorem complex.I_mul_I :

complex.I * complex.I = -1

source

theorem complex.I_mul (z : ℂ) :

complex.I * z = {re := -z.im, im := z.re}

source

theorem complex.I_ne_zero :

complex.I ≠ 0

source

theorem complex.mk_eq_add_mul_I (a b : ℝ) :

{re := a, im := b} = ↑a + ↑b * complex.I

source

@[simp]

theorem complex.re_add_im (z : ℂ) :

↑(z.re) + ↑(z.im) * complex.I = z

source

@[instance]

def complex.comm_ring :

comm_ring ℂ

Equations

complex.comm_ring = {add := has_add.add complex.has_add, add_assoc := complex.comm_ring._proof_1, zero := 0, zero_add := complex.comm_ring._proof_2, add_zero := complex.comm_ring._proof_3, neg := has_neg.neg complex.has_neg, add_left_neg := complex.comm_ring._proof_4, add_comm := complex.comm_ring._proof_5, mul := has_mul.mul complex.has_mul, mul_assoc := complex.comm_ring._proof_6, one := 1, one_mul := complex.comm_ring._proof_7, mul_one := complex.comm_ring._proof_8, left_distrib := complex.comm_ring._proof_9, right_distrib := complex.comm_ring._proof_10, mul_comm := complex.comm_ring._proof_11}

source

@[instance]

def complex.re.is_add_group_hom :

is_add_group_hom complex.re

Equations

complex.re.is_add_group_hom = is_add_group_hom.mk

source

@[instance]

def complex.im.is_add_group_hom :

is_add_group_hom complex.im

Equations

complex.im.is_add_group_hom = is_add_group_hom.mk

source

def complex.conj :

ℂ →+* ℂ

The complex conjugate.

Equations

complex.conj = {to_fun := λ (z : ℂ), {re := z.re, im := -z.im}, map_one' := complex.conj._proof_1, map_mul' := complex.conj._proof_2, map_zero' := complex.conj._proof_3, map_add' := complex.conj._proof_4}