mathlib documentation

data.complex.basic

The complex numbers #

The complex numbers are modelled as ℝ^2 in the obvious way and it is shown that they form a field of characteristic zero. The result that the complex numbers are algebraically closed, see field_theory.algebraic_closure.

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
theorem complex.of_real_def (r : ) :
r = {re := 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
@[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.of_real_mul_re (r : ) (z : ) :
((r) * z).re = r * z.re
theorem complex.of_real_mul_im (r : ) (z : ) :
((r) * z).im = r * z.im
theorem complex.of_real_mul' (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
@[instance]

This shortcut instance ensures we do not find ring via the noncomputable complex.field 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
@[instance]
Equations

Norm squared #

The norm squared function.

Equations
theorem complex.norm_sq_apply (z : ) :
complex.norm_sq z = (z.re) * z.re + (z.im) * z.im
@[simp]
@[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]
@[simp]
theorem complex.of_real_inv (r : ) :
theorem complex.inv_zero  :
0⁻¹ = 0
theorem complex.mul_inv_cancel {z : } (h : z 0) :
z * 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 : ) :
theorem complex.div_im (z 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

A complex number z plus its conjugate conj z is 2 times its real part.

theorem complex.im_eq_sub_conj (z : ) :

A complex number z minus its conjugate conj z is 2i times its imaginary part.

Absolute value #

def complex.abs (z : ) :

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 : } (h : 0 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 : ) :
theorem complex.abs_add (z w : ) :

The triangle inequality for complex numbers.

@[simp]
theorem complex.abs_abs (z : ) :
@[simp]
theorem complex.abs_pos {z : } :
@[simp]
theorem complex.abs_neg (z : ) :
theorem complex.abs_sub_comm (z w : ) :
theorem complex.abs_sub_le (a b c : ) :
@[simp]
@[simp]
theorem complex.abs_div (z w : ) :
@[simp]
@[simp]

We put a partial order on ℂ so that z ≤ w exactly if w - z is real and nonnegative. Complex numbers with different imaginary parts are incomparable.

Equations
theorem complex.le_def {z w : } :
z w ∃ (x : ), 0 x w = z + x
theorem complex.lt_def {z w : } :
z < w ∃ (x : ), 0 < x w = z + x
@[simp]
theorem complex.real_le_real {x y : } :
x y x y
@[simp]
theorem complex.real_lt_real {x y : } :
x < y x < y
@[simp]
theorem complex.zero_le_real {x : } :
0 x 0 x
@[simp]
theorem complex.zero_lt_real {x : } :
0 < x 0 < x

With z ≤ w iff w - z is real and nonnegative, is an ordered ring.

Equations

With z ≤ w iff w - z is real and nonnegative, is a star ordered ring. (That is, an ordered ring in which every element of the form star z * z is nonnegative.)

In fact, the nonnegative elements are precisely those of this form. This hold in any C^*-algebra, e.g. , but we don't yet have C^*-algebras in mathlib.

Equations

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)