# mathlib3documentation

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 `real`s: a real part `re` and an imaginary part `im`.

Instances for `complex`
@[protected, instance]
noncomputable def complex.decidable_eq  :
Equations
@[simp]
theorem complex.equiv_real_prod_apply (z : ) :
= (z.re, z.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.re z.im = w.im z = w
theorem complex.ext_iff {z w : } :
z = w z.re = w.re z.im = w.im
@[simp]
theorem complex.range_re  :
@[simp]
theorem complex.range_im  :
@[protected, instance]
def complex.has_coe  :
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  :
(λ (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 : ) :
(bit0 r) =
@[simp, norm_cast]
theorem complex.of_real_bit1 (r : ) :
(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_I  :
theorem complex.I_mul (z : ) :
= {re := -z.im, im := z.re}
theorem complex.mk_eq_add_mul_I (a b : ) :
{re := a, im := b} = a +
@[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]
def complex.ring  :

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

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

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

### 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 : ) :
( z).re = z.re
@[simp]
theorem complex.conj_im (z : ) :
( z).im = -z.im
theorem complex.conj_of_real (r : ) :
r = r
@[simp]
theorem complex.conj_I  :
theorem complex.conj_bit0 (z : ) :
(bit0 z) = bit0 ( z)
theorem complex.conj_bit1 (z : ) :
(bit1 z) = bit1 ( z)
@[simp]
theorem complex.conj_neg_I  :
theorem complex.conj_eq_iff_real {z : } :
z = z (r : ), z = r
theorem complex.conj_eq_iff_re {z : } :
z = z (z.re) = z
theorem complex.conj_eq_iff_im {z : } :
z = z z.im = 0
@[simp, nolint]
theorem complex.star_def  :

### Norm squared #

def complex.norm_sq  :

The norm squared function.

Equations
theorem complex.norm_sq_apply (z : ) :
= z.re * z.re + z.im * z.im
@[simp]
theorem complex.norm_sq_of_real (r : ) :
= r * r
@[simp]
theorem complex.norm_sq_mk (x y : ) :
complex.norm_sq {re := x, im := y} = x * x + y * y
theorem complex.norm_sq_add_mul_I (x y : ) :
@[simp]
theorem complex.norm_sq_zero  :
@[simp]
theorem complex.norm_sq_one  :
@[simp]
theorem complex.norm_sq_I  :
theorem complex.norm_sq_nonneg (z : ) :
@[simp]
theorem complex.norm_sq_eq_zero {z : } :
z = 0
@[simp]
theorem complex.norm_sq_pos {z : } :
z 0
@[simp]
theorem complex.norm_sq_neg (z : ) :
@[simp]
theorem complex.norm_sq_conj (z : ) :
theorem complex.norm_sq_mul (z w : ) :
theorem complex.norm_sq_add (z w : ) :
complex.norm_sq (z + w) = + 2 * (z * w).re
theorem complex.re_sq_le_norm_sq (z : ) :
z.re * z.re
theorem complex.im_sq_le_norm_sq (z : ) :
z.im * z.im
theorem complex.mul_conj (z : ) :
z * z =
theorem complex.add_conj (z : ) :
z + z = (2 * z.re)
def complex.of_real  :

The coercion `ℝ → ℂ` as a `ring_hom`.

Equations
@[simp]
theorem complex.of_real_eq_coe (r : ) :
@[simp]
theorem complex.I_sq  :
= -1
@[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
theorem complex.sub_conj (z : ) :
z - z = (2 * z.im) * complex.I
theorem complex.norm_sq_sub (z w : ) :
complex.norm_sq (z - w) = - 2 * (z * w).re

### Inversion #

@[protected, instance]
noncomputable def complex.has_inv  :
Equations
theorem complex.inv_def (z : ) :
z⁻¹ = z *
@[simp]
theorem complex.inv_re (z : ) :
@[simp]
theorem complex.inv_im (z : ) :
@[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 : ) :
= (-1) ^ n
@[simp]
theorem complex.I_zpow_bit1 (n : ) :
= (-1) ^ n * complex.I
theorem complex.div_re (z w : ) :
(z / w).re = z.re * w.re / + z.im * w.im /
theorem complex.div_im (z w : ) :
(z / w).im = z.im * w.re / - z.re * w.im /
theorem complex.conj_inv (x : ) :
= ( x)⁻¹
@[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 : ) :
@[simp]
theorem complex.inv_I  :
@[simp]
theorem complex.norm_sq_inv (z : ) :
@[simp]
theorem complex.norm_sq_div (z w : ) :

### 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 + z) / 2

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

theorem complex.im_eq_sub_conj (z : ) :
(z.im) = (z - z) / (2 * complex.I)

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
theorem complex.abs_def  :
complex.abs = λ (z : ),
theorem complex.abs_apply {z : } :
@[simp, norm_cast]
theorem complex.abs_of_real (r : ) :
theorem complex.abs_of_nonneg {r : } (h : 0 r) :
theorem complex.abs_of_nat (n : ) :
theorem complex.mul_self_abs (z : ) :
theorem complex.sq_abs (z : ) :
@[simp]
theorem complex.sq_abs_sub_sq_re (z : ) :
- z.re ^ 2 = z.im ^ 2
@[simp]
theorem complex.sq_abs_sub_sq_im (z : ) :
- z.im ^ 2 = z.re ^ 2
@[simp]
theorem complex.abs_I  :
@[simp]
theorem complex.abs_two  :
@[simp]
theorem complex.range_abs  :
@[simp]
theorem complex.abs_conj (z : ) :
@[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.abs_re_le_abs (z : ) :
theorem complex.abs_im_le_abs (z : ) :
theorem complex.re_le_abs (z : ) :
z.re
theorem complex.im_le_abs (z : ) :
z.im
@[simp]
theorem complex.abs_re_lt_abs {z : } :
z.im 0
@[simp]
theorem complex.abs_im_lt_abs {z : } :
z.re 0
@[simp]
theorem complex.abs_abs (z : ) :
@[simp, norm_cast]
theorem complex.abs_cast_nat (n : ) :
@[simp, norm_cast]
theorem complex.int_cast_abs (n : ) :
theorem complex.norm_sq_eq_abs (x : ) :
@[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 strictly ordered ring.

Equations
@[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 #

theorem complex.is_cau_seq_re (f : complex.abs) :
(λ (n : ), (f n).re)
theorem complex.is_cau_seq_im (f : complex.abs) :
(λ (n : ), (f n).im)
noncomputable def complex.cau_seq_re (f : complex.abs) :

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

Equations
noncomputable def complex.cau_seq_im (f : complex.abs) :

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

Equations
theorem complex.is_cau_seq_abs {f : } (hf : f) :
noncomputable def complex.lim_aux (f : complex.abs) :

The limit of a Cauchy sequence of complex numbers.

Equations
@[protected, instance]
theorem complex.is_cau_seq_conj (f : complex.abs) :
(λ (n : ), (f n))
noncomputable def complex.cau_seq_conj (f : complex.abs) :

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

Equations
noncomputable def complex.cau_seq_abs (f : complex.abs) :

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)