mathlib3 documentation

data.complex.basic

The complex numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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  :

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

Instances for complex
@[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.re z.im = w.im z = 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]
def complex.can_lift  :
can_lift coe (λ (z : ), z.im = 0)
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]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]

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

Equations
@[protected, instance]

This shortcut instance ensures we do not find comm_semiring 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 : ) :
@[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 #

@[protected, instance]
noncomputable def complex.field  :
Equations
@[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  :

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

Equations
@[simp, norm_cast]
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_two  :
@[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 : ) :
@[simp]
theorem complex.abs_re_lt_abs {z : } :
@[simp]
theorem complex.abs_im_lt_abs {z : } :
@[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
theorem complex.eq_re_of_real_le {r : } {z : } (hz : r z) :
z = (z.re)
@[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)