mathlib documentation

data.complex.basic

The complex numbers

The complex numbers are modelled as ℝ^2 in the obvious way.

Definition and basic arithmmetic

structure complex  :
Type

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

The equivalence between the complex numbers and ℝ × ℝ.

Equations
@[simp]
theorem complex.eta (z : ) :
{re := z.re, im := z.im} = z

@[ext]
theorem complex.ext {z w : } :
z.re = w.rez.im = w.imz = w

theorem complex.ext_iff {z w : } :
z = w z.re = w.re z.im = w.im

@[instance]

Equations
@[simp]
theorem complex.of_real_re (r : ) :
r.re = r

@[simp]
theorem complex.of_real_im (r : ) :
r.im = 0

@[simp]
theorem complex.of_real_inj {z w : } :
z = w z = w

@[instance]

Equations
@[instance]

Equations
@[simp]
theorem complex.zero_re  :
0.re = 0

@[simp]
theorem complex.zero_im  :
0.im = 0

@[simp]
theorem complex.of_real_zero  :
0 = 0

@[simp]
theorem complex.of_real_eq_zero {z : } :
z = 0 z = 0

theorem complex.of_real_ne_zero {z : } :
z 0 z 0

@[instance]

Equations
@[simp]
theorem complex.one_re  :
1.re = 1

@[simp]
theorem complex.one_im  :
1.im = 0

@[simp]
theorem complex.of_real_one  :
1 = 1

@[instance]

Equations
@[simp]
theorem complex.add_re (z w : ) :
(z + w).re = z.re + w.re

@[simp]
theorem complex.add_im (z w : ) :
(z + w).im = z.im + w.im

@[simp]
theorem complex.bit0_re (z : ) :
(bit0 z).re = bit0 z.re

@[simp]
theorem complex.bit1_re (z : ) :
(bit1 z).re = bit1 z.re

@[simp]
theorem complex.bit0_im (z : ) :
(bit0 z).im = bit0 z.im

@[simp]
theorem complex.bit1_im (z : ) :
(bit1 z).im = bit0 z.im

@[simp]
theorem complex.of_real_add (r s : ) :
(r + s) = r + s

@[simp]
theorem complex.of_real_bit0 (r : ) :

@[simp]
theorem complex.of_real_bit1 (r : ) :

@[instance]

Equations
@[simp]
theorem complex.neg_re (z : ) :
(-z).re = -z.re

@[simp]
theorem complex.neg_im (z : ) :
(-z).im = -z.im

@[simp]
theorem complex.of_real_neg (r : ) :

@[instance]

Equations
@[simp]
theorem complex.mul_re (z w : ) :
(z * w).re = (z.re) * w.re - (z.im) * w.im

@[simp]
theorem complex.mul_im (z w : ) :
(z * w).im = (z.re) * w.im + (z.im) * w.re

@[simp]
theorem complex.of_real_mul (r s : ) :
r * s = (r) * s

theorem complex.smul_re (r : ) (z : ) :
((r) * z).re = r * z.re

theorem complex.smul_im (r : ) (z : ) :
((r) * z).im = r * z.im

theorem complex.of_real_smul (r : ) (z : ) :
(r) * z = {re := r * z.re, im := r * z.im}

The imaginary unit, I

def complex.I  :

The imaginary unit.

Equations
@[simp]
theorem complex.I_re  :

@[simp]
theorem complex.I_im  :

@[simp]

theorem complex.I_mul (z : ) :
complex.I * z = {re := -z.im, im := z.re}

theorem complex.mk_eq_add_mul_I (a b : ) :
{re := a, im := b} = a + (b) * complex.I

@[simp]
theorem complex.re_add_im (z : ) :
(z.re) + ((z.im)) * complex.I = z

Commutative ring instance and lemmas

@[instance]

Equations
@[simp]
theorem complex.I_pow_bit0 (n : ) :
complex.I ^ bit0 n = (-1) ^ n

@[simp]
theorem complex.I_pow_bit1 (n : ) :

Complex conjugation

The complex conjugate.

Equations
@[simp]
theorem complex.conj_re (z : ) :

@[simp]
theorem complex.conj_im (z : ) :

@[simp]

@[simp]

@[simp]
theorem complex.conj_eq_zero {z : } :

theorem complex.eq_conj_iff_real {z : } :
complex.conj z = z ∃ (r : ), z = r

Norm squared

def complex.norm_sq  :

The norm squared function.

Equations
@[simp]

@[simp]

@[simp]

@[simp]
theorem complex.norm_sq_eq_zero {z : } :

@[simp]
theorem complex.norm_sq_pos {z : } :

theorem complex.add_conj (z : ) :

@[simp]
theorem complex.I_sq  :

@[simp]
theorem complex.sub_re (z w : ) :
(z - w).re = z.re - w.re

@[simp]
theorem complex.sub_im (z w : ) :
(z - w).im = z.im - w.im

@[simp]
theorem complex.of_real_sub (r s : ) :
(r - s) = r - s

@[simp]
theorem complex.of_real_pow (r : ) (n : ) :
(r ^ n) = r ^ n

Inversion

@[instance]

Equations
@[simp]
theorem complex.inv_re (z : ) :

@[simp]
theorem complex.inv_im (z : ) :

@[simp]
theorem complex.of_real_inv (r : ) :

theorem complex.inv_zero  :
0⁻¹ = 0

theorem complex.mul_inv_cancel {z : } :
z 0z * z⁻¹ = 1

Field instance and lemmas

@[simp]
theorem complex.I_fpow_bit0 (n : ) :
complex.I ^ bit0 n = (-1) ^ n

@[simp]
theorem complex.I_fpow_bit1 (n : ) :

theorem complex.div_re (z w : ) :
(z / w).re = (z.re) * w.re / complex.norm_sq w + (z.im) * w.im / complex.norm_sq w

theorem complex.div_im (z w : ) :
(z / w).im = (z.im) * w.re / complex.norm_sq w - (z.re) * w.im / complex.norm_sq w

@[simp]
theorem complex.of_real_div (r s : ) :
(r / s) = r / s

@[simp]
theorem complex.of_real_fpow (r : ) (n : ) :
(r ^ n) = r ^ n

@[simp]
theorem complex.div_I (z : ) :

Cast lemmas

@[simp]
theorem complex.of_real_nat_cast (n : ) :

@[simp]
theorem complex.nat_cast_re (n : ) :

@[simp]
theorem complex.nat_cast_im (n : ) :
n.im = 0

@[simp]
theorem complex.of_real_int_cast (n : ) :

@[simp]
theorem complex.int_cast_re (n : ) :

@[simp]
theorem complex.int_cast_im (n : ) :
n.im = 0

@[simp]
theorem complex.of_real_rat_cast (n : ) :

@[simp]
theorem complex.rat_cast_re (q : ) :

@[simp]
theorem complex.rat_cast_im (q : ) :
q.im = 0

Characteristic zero

theorem complex.re_eq_add_conj (z : ) :
(z.re) = (z + complex.conj z) / 2

Absolute value

def complex.abs  :

The complex absolute value function, defined as the square root of the norm squared.

Equations
@[simp]
theorem complex.abs_of_real (r : ) :

theorem complex.abs_of_nonneg {r : } :
0 rcomplex.abs r = r

@[simp]
theorem complex.abs_zero  :

@[simp]
theorem complex.abs_one  :

@[simp]

@[simp]
theorem complex.abs_two  :

@[simp]
theorem complex.abs_eq_zero {z : } :
complex.abs z = 0 z = 0

theorem complex.abs_ne_zero {z : } :

@[simp]
theorem complex.abs_mul (z w : ) :

theorem complex.re_le_abs (z : ) :

theorem complex.im_le_abs (z : ) :

@[simp]
theorem complex.abs_abs (z : ) :

@[simp]
theorem complex.abs_pos {z : } :

@[simp]
theorem complex.abs_neg (z : ) :

theorem complex.abs_sub (z w : ) :

theorem complex.abs_sub_le (a b c : ) :

@[simp]

@[simp]
theorem complex.abs_div (z w : ) :

@[simp]

Cauchy sequences

The real part of a complex Cauchy sequence, as a real Cauchy sequence.

Equations

The imaginary part of a complex Cauchy sequence, as a real Cauchy sequence.

Equations

The limit of a Cauchy sequence of complex numbers.

Equations
@[instance]

Equations

The complex conjugate of a complex Cauchy sequence, as a complex Cauchy sequence.

Equations

The absolute value of a complex Cauchy sequence, as a real Cauchy sequence.

Equations
@[simp]
theorem complex.of_real_prod {α : Type u_1} (s : finset α) (f : α → ) :
∏ (i : α) in s, f i = ∏ (i : α) in s, (f i)

@[simp]
theorem complex.of_real_sum {α : Type u_1} (s : finset α) (f : α → ) :
∑ (i : α) in s, f i = ∑ (i : α) in s, (f i)