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 #

@[protected, instance]
noncomputable def complex.decidable_eq  :
Equations

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
@[protected, instance]
Equations
@[simp, norm_cast]
theorem complex.of_real_re (r : ) :
r.re = r
@[simp, norm_cast]
theorem complex.of_real_im (r : ) :
r.im = 0
theorem complex.of_real_def (r : ) :
r = {re := r, im := 0}
@[simp, norm_cast]
theorem complex.of_real_inj {z w : } :
z = w z = w
@[protected, instance]
Equations
def set.re_prod_im (s t : set ) :

The product of a set on the real axis and a set on the imaginary axis of the complex plane, denoted by s ×ℂ t.

Equations
theorem complex.mem_re_prod_im {z : } {s t : set } :
z s ×ℂ t z.re s z.im t
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem complex.zero_re  :
0.re = 0
@[simp]
theorem complex.zero_im  :
0.im = 0
@[simp, norm_cast]
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
@[protected, instance]
Equations
@[simp]
theorem complex.one_re  :
1.re = 1
@[simp]
theorem complex.one_im  :
1.im = 0
@[simp, norm_cast]
theorem complex.of_real_one  :
1 = 1
@[simp]
theorem complex.of_real_eq_one {z : } :
z = 1 z = 1
theorem complex.of_real_ne_one {z : } :
z 1 z 1
@[protected, 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, norm_cast]
theorem complex.of_real_add (r s : ) :
(r + s) = r + s
@[simp, norm_cast]
theorem complex.of_real_bit0 (r : ) :
@[simp, norm_cast]
theorem complex.of_real_bit1 (r : ) :
@[protected, instance]
Equations
@[simp]
theorem complex.neg_re (z : ) :
(-z).re = -z.re
@[simp]
theorem complex.neg_im (z : ) :
(-z).im = -z.im
@[simp, norm_cast]
theorem complex.of_real_neg (r : ) :
@[protected, instance]
Equations
@[protected, 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, norm_cast]
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
theorem complex.mul_I_re (z : ) :
theorem complex.mul_I_im (z : ) :
(z * complex.I).im = z.re
theorem complex.I_mul_re (z : ) :
theorem complex.I_mul_im (z : ) :
(complex.I * z).im = z.re

Commutative ring instance and lemmas #

@[protected, instance]
Equations
@[protected, instance]

This shortcut instance ensures we do not find add_comm_group via the noncomputable complex.normed_group instance.

Equations
@[protected, instance]

This shortcut instance ensures we do not find ring via the noncomputable complex.field instance.

Equations

The "real part" map, considered as an additive group homomorphism.

Equations

The "imaginary part" map, considered as an additive group homomorphism.

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

Complex conjugation #

@[protected, instance]

This defines the complex conjugate as the star operation of the star_ring. It is recommended to use the ring endomorphism version star_ring_end, available under the notation conj in the locale complex_conjugate.

Equations
@[simp]
theorem complex.conj_re (z : ) :
@[simp]
theorem complex.conj_im (z : ) :
theorem complex.eq_conj_iff_real {z : } :
(star_ring_end ) z = z ∃ (r : ), z = r
@[simp, nolint]

Norm squared #

The norm squared function.

Equations
theorem complex.norm_sq_apply (z : ) :
@[simp]
@[simp]
theorem complex.norm_sq_mk (x y : ) :
complex.norm_sq {re := x, im := y} = x * x + y * y
@[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, norm_cast]
theorem complex.of_real_sub (r s : ) :
(r - s) = r - s
@[simp, norm_cast]
theorem complex.of_real_pow (r : ) (n : ) :
(r ^ n) = r ^ n

Inversion #

@[protected, instance]
noncomputable def complex.has_inv  :
Equations
@[simp]
theorem complex.inv_re (z : ) :
@[simp]
@[simp, norm_cast]
theorem complex.of_real_inv (r : ) :
@[protected]
theorem complex.inv_zero  :
0⁻¹ = 0
@[protected]
theorem complex.mul_inv_cancel {z : } (h : z 0) :
z * z⁻¹ = 1

Field instance and lemmas #

@[simp]
theorem complex.I_zpow_bit0 (n : ) :
complex.I ^ bit0 n = (-1) ^ n
@[simp]
theorem complex.I_zpow_bit1 (n : ) :
theorem complex.div_re (z w : ) :
theorem complex.div_im (z w : ) :
@[simp, norm_cast]
theorem complex.of_real_div (r s : ) :
(r / s) = r / s
@[simp, norm_cast]
theorem complex.of_real_zpow (r : ) (n : ) :
(r ^ n) = r ^ n
@[simp]
theorem complex.div_I (z : ) :

Cast lemmas #

@[simp, norm_cast]
theorem complex.of_real_nat_cast (n : ) :
@[simp, norm_cast]
theorem complex.nat_cast_re (n : ) :
@[simp, norm_cast]
theorem complex.nat_cast_im (n : ) :
n.im = 0
@[simp, norm_cast]
theorem complex.of_real_int_cast (n : ) :
@[simp, norm_cast]
theorem complex.int_cast_re (n : ) :
@[simp, norm_cast]
theorem complex.int_cast_im (n : ) :
n.im = 0
@[simp, norm_cast]
theorem complex.of_real_rat_cast (n : ) :
@[simp, norm_cast]
theorem complex.rat_cast_re (q : ) :
@[simp, norm_cast]
theorem complex.rat_cast_im (q : ) :
q.im = 0

Characteristic zero #

@[protected, instance]
theorem complex.re_eq_add_conj (z : ) :
(z.re) = (z + (star_ring_end ) 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 #

noncomputable def complex.abs (z : ) :

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

Equations
Instances for complex.abs
@[simp, norm_cast]
theorem complex.abs_of_real (r : ) :
theorem complex.abs_of_nonneg {r : } (h : 0 r) :
@[simp]
theorem complex.sq_abs_sub_sq_re (z : ) :
complex.abs z ^ 2 - z.re ^ 2 = z.im ^ 2
@[simp]
theorem complex.sq_abs_sub_sq_im (z : ) :
complex.abs z ^ 2 - z.im ^ 2 = z.re ^ 2
@[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 : ) :
@[simp]
theorem complex.abs_prod {ι : Type u_1} (s : finset ι) (f : ι → ) :
complex.abs (s.prod f) = s.prod (λ (i : ι), complex.abs (f i))
@[simp]
theorem complex.abs_pow (z : ) (n : ) :
@[simp]
theorem complex.abs_zpow (z : ) (n : ) :
theorem complex.re_le_abs (z : ) :
theorem complex.im_le_abs (z : ) :
@[simp]
theorem complex.abs_re_lt_abs {z : } :
@[simp]
theorem complex.abs_im_lt_abs {z : } :
theorem complex.abs_add (z w : ) :

The triangle inequality for complex numbers.

@[simp]
@[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, norm_cast]
@[simp, norm_cast]
@[protected]

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 z.re w.re z.im = w.im
theorem complex.lt_def {z w : } :
z < w z.re < w.re z.im = w.im
@[simp, norm_cast]
theorem complex.real_le_real {x y : } :
x y x y
@[simp, norm_cast]
theorem complex.real_lt_real {x y : } :
x < y x < y
@[simp, norm_cast]
theorem complex.zero_le_real {x : } :
0 x 0 x
@[simp, norm_cast]
theorem complex.zero_lt_real {x : } :
0 < x 0 < x
theorem complex.not_le_iff {z w : } :
¬z w w.re < z.re z.im w.im
theorem complex.not_lt_iff {z w : } :
¬z < w w.re z.re z.im w.im
theorem complex.not_le_zero_iff {z : } :
¬z 0 0 < z.re z.im 0
theorem complex.not_lt_zero_iff {z : } :
¬z < 0 0 z.re z.im 0
@[protected]

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

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
noncomputable def complex.lim_aux (f : cau_seq complex.abs) :

The limit of a Cauchy sequence of complex numbers.

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, norm_cast]
theorem complex.of_real_prod {α : Type u_1} (s : finset α) (f : α → ) :
(s.prod (λ (i : α), f i)) = s.prod (λ (i : α), (f i))
@[simp, norm_cast]
theorem complex.of_real_sum {α : Type u_1} (s : finset α) (f : α → ) :
(s.sum (λ (i : α), f i)) = s.sum (λ (i : α), (f i))
@[simp]
theorem complex.re_sum {α : Type u_1} (s : finset α) (f : α → ) :
(s.sum (λ (i : α), f i)).re = s.sum (λ (i : α), (f i).re)
@[simp]
theorem complex.im_sum {α : Type u_1} (s : finset α) (f : α → ) :
(s.sum (λ (i : α), f i)).im = s.sum (λ (i : α), (f i).im)