# Documentation

Mathlib.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 FieldTheory.AlgebraicClosure.

### Definition and basic arithmetic #

structure Complex :

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

Instances For
Instances For
noncomputable instance Complex.instDecidableEqComplex :
@[simp]
theorem Complex.equivRealProd_apply (z : ) :
= (z.re, z.im)

The equivalence between the complex numbers and ℝ × ℝ.

Instances For
@[simp]
theorem Complex.eta (z : ) :
{ re := z.re, im := z.im } = z
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
@[simp]
theorem Complex.range_re :
= Set.univ
@[simp]
theorem Complex.range_im :
= Set.univ

The natural inclusion of the real numbers into the complex numbers. The name Complex.ofReal is reserved for the bundled homomorphism.

Instances For
@[simp]
theorem Complex.ofReal_re (r : ) :
(r).re = r
@[simp]
theorem Complex.ofReal_im (r : ) :
(r).im = 0
theorem Complex.ofReal_def (r : ) :
r = { re := r, im := 0 }
@[simp]
theorem Complex.ofReal_inj {z : } {w : } :
z = w z = w
def Complex.Set.reProdIm (s : ) (t : ) :

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

Instances For
Instances For
theorem Complex.mem_reProdIm {z : } {s : } {t : } :
z s ×ℂ t z.re s z.im t
@[simp]
theorem Complex.zero_re :
0.re = 0
@[simp]
theorem Complex.zero_im :
0.im = 0
@[simp]
theorem Complex.ofReal_zero :
0 = 0
@[simp]
theorem Complex.ofReal_eq_zero {z : } :
z = 0 z = 0
theorem Complex.ofReal_ne_zero {z : } :
z 0 z 0
@[simp]
theorem Complex.one_re :
1.re = 1
@[simp]
theorem Complex.one_im :
1.im = 0
@[simp]
theorem Complex.ofReal_one :
1 = 1
@[simp]
theorem Complex.ofReal_eq_one {z : } :
z = 1 z = 1
theorem Complex.ofReal_ne_one {z : } :
z 1 z 1
@[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.ofReal_add (r : ) (s : ) :
↑(r + s) = r + s
@[simp]
theorem Complex.ofReal_bit0 (r : ) :
↑(bit0 r) = bit0 r
@[simp]
theorem Complex.ofReal_bit1 (r : ) :
↑(bit1 r) = bit1 r
@[simp]
theorem Complex.neg_re (z : ) :
(-z).re = -z.re
@[simp]
theorem Complex.neg_im (z : ) :
(-z).im = -z.im
@[simp]
theorem Complex.ofReal_neg (r : ) :
↑(-r) = -r
@[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.ofReal_mul (r : ) (s : ) :
↑(r * s) = r * s
theorem Complex.ofReal_mul_re (r : ) (z : ) :
(r * z).re = r * z.re
theorem Complex.ofReal_mul_im (r : ) (z : ) :
(r * z).im = r * z.im
theorem Complex.ofReal_mul' (r : ) (z : ) :
r * z = { re := r * z.re, im := r * z.im }

### The imaginary unit, I#

The imaginary unit.

Instances For
@[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 : ) :
().re = -z.im
theorem Complex.mul_I_im (z : ) :
().im = z.re
theorem Complex.I_mul_re (z : ) :
().re = -z.im
theorem Complex.I_mul_im (z : ) :
().im = z.re
@[simp]
theorem Complex.equivRealProd_symm_apply (p : ) :
p = p.fst + p.snd * Complex.I

### Commutative ring instance and lemmas #

instance Complex.instSMulRealComplex {R : Type u_1} [] :
theorem Complex.smul_re {R : Type u_1} [] (r : R) (z : ) :
(r z).re = r z.re
theorem Complex.smul_im {R : Type u_1} [] (r : R) (z : ) :
(r z).im = r z.im
@[simp]
theorem Complex.real_smul {x : } {z : } :
x z = x * z

This shortcut instance ensures we do not find Ring via the noncomputable Complex.field instance.

This shortcut instance ensures we do not find CommSemiring via the noncomputable Complex.field instance.

This shortcut instance ensures we do not find Semiring via the noncomputable Complex.field instance.

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

Instances For
@[simp]

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

Instances For
@[simp]
@[simp]
theorem Complex.I_pow_bit0 (n : ) :
= (-1) ^ n
@[simp]
theorem Complex.I_pow_bit1 (n : ) :
= (-1) ^ n * Complex.I
@[simp]
theorem Complex.ofReal_ofNat (n : ) [] :
↑() =
@[simp]
theorem Complex.re_ofNat (n : ) [] :
().re =
@[simp]
theorem Complex.im_ofNat (n : ) [] :
().im = 0

### Complex conjugation #

This defines the complex conjugate as the star operation of the StarRing ℂ. It is recommended to use the ring endomorphism version starRingEnd, available under the notation conj in the locale ComplexConjugate.

@[simp]
theorem Complex.conj_re (z : ) :
(↑() z).re = z.re
@[simp]
theorem Complex.conj_im (z : ) :
(↑() z).im = -z.im
theorem Complex.conj_ofReal (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)
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]
theorem Complex.star_def :
star = ↑()

### Norm squared #

The norm squared function.

Instances For
theorem Complex.normSq_apply (z : ) :
= z.re * z.re + z.im * z.im
@[simp]
theorem Complex.normSq_ofReal (r : ) :
= r * r
@[simp]
theorem Complex.normSq_mk (x : ) (y : ) :
Complex.normSq { re := x, im := y } = x * x + y * y
theorem Complex.normSq_add_mul_I (x : ) (y : ) :
Complex.normSq (x + ) = x ^ 2 + y ^ 2
theorem Complex.normSq_eq_conj_mul_self {z : } :
↑() = ↑() z * z
@[simp]
@[simp]
theorem Complex.normSq_eq_zero {z : } :
= 0 z = 0
@[simp]
theorem Complex.normSq_pos {z : } :
0 < z 0
@[simp]
theorem Complex.normSq_neg (z : ) :
@[simp]
theorem Complex.normSq_conj (z : ) :
Complex.normSq (↑() z) =
theorem Complex.normSq_mul (z : ) (w : ) :
Complex.normSq (z * w) =
theorem Complex.normSq_add (z : ) (w : ) :
Complex.normSq (z + w) = + 2 * (z * ↑() w).re
theorem Complex.re_sq_le_normSq (z : ) :
z.re * z.re
theorem Complex.im_sq_le_normSq (z : ) :
z.im * z.im
theorem Complex.mul_conj (z : ) :
z * ↑() z = ↑()
theorem Complex.add_conj (z : ) :
z + ↑() z = ↑(2 * z.re)

The coercion ℝ → ℂ as a RingHom.

Instances For
@[simp]
theorem Complex.ofReal_eq_coe (r : ) :
= 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]
theorem Complex.ofReal_sub (r : ) (s : ) :
↑(r - s) = r - s
@[simp]
theorem Complex.ofReal_pow (r : ) (n : ) :
↑(r ^ n) = r ^ n
theorem Complex.sub_conj (z : ) :
z - ↑() z = ↑(2 * z.im) * Complex.I
theorem Complex.normSq_sub (z : ) (w : ) :
Complex.normSq (z - w) = - 2 * (z * ↑() w).re

### Inversion #

noncomputable instance Complex.instInvComplex :
theorem Complex.inv_def (z : ) :
z⁻¹ = ↑() z * ()⁻¹
@[simp]
theorem Complex.inv_re (z : ) :
z⁻¹.re = z.re /
@[simp]
theorem Complex.inv_im (z : ) :
z⁻¹.im = -z.im /
@[simp]
theorem Complex.ofReal_inv (r : ) :
r⁻¹ = (r)⁻¹
theorem Complex.mul_inv_cancel {z : } (h : z 0) :
z * z⁻¹ = 1
noncomputable instance Complex.instRatCastComplex :

### Cast lemmas #

@[simp]
theorem Complex.ofReal_nat_cast (n : ) :
n = n
@[simp]
theorem Complex.nat_cast_re (n : ) :
(n).re = n
@[simp]
theorem Complex.nat_cast_im (n : ) :
(n).im = 0
@[simp]
theorem Complex.ofReal_int_cast (n : ) :
n = n
@[simp]
theorem Complex.int_cast_re (n : ) :
(n).re = n
@[simp]
theorem Complex.int_cast_im (n : ) :
(n).im = 0
@[simp]
theorem Complex.rat_cast_im (q : ) :
(q).im = 0
@[simp]
theorem Complex.rat_cast_re (q : ) :
(q).re = q

### Field instance and lemmas #

noncomputable instance Complex.instField :
@[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⁻¹ = (↑() x)⁻¹
@[simp]
theorem Complex.ofReal_div (r : ) (s : ) :
↑(r / s) = r / s
@[simp]
theorem Complex.ofReal_zpow (r : ) (n : ) :
↑(r ^ n) = r ^ n
@[simp]
theorem Complex.div_I (z : ) :
= -()
@[simp]
theorem Complex.inv_I :
theorem Complex.normSq_div (z : ) (w : ) :
Complex.normSq (z / w) =
@[simp]
theorem Complex.ofReal_rat_cast (n : ) :
n = n

### Characteristic zero #

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) / ()

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.

Instances For
theorem Complex.abs_def :
= fun z =>
theorem Complex.abs_apply {z : } :
=
@[simp]
theorem Complex.abs_ofReal (r : ) :
Complex.abs r = |r|
theorem Complex.abs_of_nonneg {r : } (h : 0 r) :
Complex.abs r = r
theorem Complex.abs_of_nat (n : ) :
Complex.abs n = n
theorem Complex.sq_abs (z : ) :
^ 2 =
@[simp]
theorem Complex.sq_abs_sub_sq_re (z : ) :
^ 2 - z.re ^ 2 = z.im ^ 2
@[simp]
theorem Complex.sq_abs_sub_sq_im (z : ) :
^ 2 - z.im ^ 2 = z.re ^ 2
@[simp]
theorem Complex.abs_I :
@[simp]
theorem Complex.abs_two :
= 2
@[simp]
@[simp]
theorem Complex.abs_conj (z : ) :
Complex.abs (↑() z) =
@[simp]
theorem Complex.abs_prod {ι : Type u_1} (s : ) (f : ι) :
Complex.abs () = Finset.prod s fun I => Complex.abs (f I)
theorem Complex.abs_pow (z : ) (n : ) :
Complex.abs (z ^ n) = ^ n
theorem Complex.abs_zpow (z : ) (n : ) :
Complex.abs (z ^ n) = ^ n
theorem Complex.abs_re_le_abs (z : ) :
|z.re|
theorem Complex.abs_im_le_abs (z : ) :
|z.im|
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.re| < z.im 0
@[simp]
theorem Complex.abs_im_lt_abs {z : } :
|z.im| < z.re 0
@[simp]
theorem Complex.abs_abs (z : ) :
|| =
theorem Complex.abs_le_abs_re_add_abs_im (z : ) :
|z.re| + |z.im|
theorem Complex.abs_le_sqrt_two_mul_max (z : ) :
* max |z.re| |z.im|
theorem Complex.abs_re_div_abs_le_one (z : ) :
|z.re / | 1
theorem Complex.abs_im_div_abs_le_one (z : ) :
|z.im / | 1
@[simp]
theorem Complex.abs_cast_nat (n : ) :
Complex.abs n = n
@[simp]
theorem Complex.int_cast_abs (n : ) :
|n| = Complex.abs n

### Cauchy sequences #

theorem Complex.isCauSeq_re (f : ) :
IsCauSeq abs fun n => (f n).re
theorem Complex.isCauSeq_im (f : ) :
IsCauSeq abs fun n => (f n).im
noncomputable def Complex.cauSeqRe (f : ) :

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

Instances For
noncomputable def Complex.cauSeqIm (f : ) :

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

Instances For
theorem Complex.isCauSeq_abs {f : } (hf : ) :
IsCauSeq abs ()
noncomputable def Complex.limAux (f : ) :

The limit of a Cauchy sequence of complex numbers.

Instances For
theorem Complex.equiv_limAux (f : ) :
f
theorem Complex.lim_re (f : ) :
= ().re
theorem Complex.lim_im (f : ) :
= ().im
theorem Complex.isCauSeq_conj (f : ) :
IsCauSeq fun n => ↑() (f n)
noncomputable def Complex.cauSeqConj (f : ) :

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

Instances For
theorem Complex.lim_conj (f : ) :
= ↑() ()
noncomputable def Complex.cauSeqAbs (f : ) :

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

Instances For
theorem Complex.lim_abs (f : ) :
@[simp]
theorem Complex.ofReal_prod {α : Type u_1} (s : ) (f : α) :
↑(Finset.prod s fun i => f i) = Finset.prod s fun i => ↑(f i)
@[simp]
theorem Complex.ofReal_sum {α : Type u_1} (s : ) (f : α) :
↑(Finset.sum s fun i => f i) = Finset.sum s fun i => ↑(f i)
@[simp]
theorem Complex.re_sum {α : Type u_1} (s : ) (f : α) :
(Finset.sum s fun i => f i).re = Finset.sum s fun i => (f i).re
@[simp]
theorem Complex.im_sum {α : Type u_1} (s : ) (f : α) :
(Finset.sum s fun i => f i).im = Finset.sum s fun i => (f i).im