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 #

source
structure complex  :
Type

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

source
@[protected, instance]
noncomputable def complex.decidable_eq  :
decidable_eq ℂ
Equations
source
@[simp]
theorem complex.equiv_real_prod_apply (z : ℂ) :
⇑complex.equiv_real_prod z = (z.re, z.im)
source
def complex.equiv_real_prod  :
ℂ ≃ ℝ × ℝ

The equivalence between the complex numbers and ℝ × ℝ.

Equations
source
@[simp]
theorem complex.equiv_real_prod_symm_apply_re (p : ℝ × ℝ) :
(⇑(complex.equiv_real_prod.symm) p).re = p.fst
source
@[simp]
theorem complex.equiv_real_prod_symm_apply_im (p : ℝ × ℝ) :
(⇑(complex.equiv_real_prod.symm) p).im = p.snd
source
@[simp]
theorem complex.eta (z : ℂ) :
{re := z.re, im := z.im} = z
source
@[ext]
theorem complex.ext {z w : ℂ} :
z.re = w.re → z.im = w.im → z = w
source
theorem complex.ext_iff {z w : ℂ} :
z = w ↔ z.re = w.re ∧ z.im = w.im
source
@[protected, instance]
def complex.has_coe  :
has_coe ℝ ℂ
Equations
source
@[simp, norm_cast]
theorem complex.of_real_re (r : ℝ) :
↑r.re = r
source
@[simp, norm_cast]
theorem complex.of_real_im (r : ℝ) :
↑r.im = 0
source
theorem complex.of_real_def (r : ℝ) :
↑r = {re := r, im := 0}
source
@[simp, norm_cast]
theorem complex.of_real_inj {z w : ℝ} :
↑z = ↑w ↔ z = w
source
theorem complex.of_real_injective  :
function.injective coe
source
@[protected, instance]
def complex.real.can_lift  :
can_lift ℂ ℝ
Equations
source
def set.re_prod_im (s t : set ℝ) :
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
source
theorem complex.mem_re_prod_im {z : ℂ} {s t : set ℝ} :
z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t
source
@[protected, instance]
def complex.has_zero  :
has_zero ℂ
Equations
source
@[protected, instance]
def complex.inhabited  :
inhabited ℂ
Equations
source
@[simp]
theorem complex.zero_re  :
0.re = 0
source
@[simp]
theorem complex.zero_im  :
0.im = 0
source
@[simp, norm_cast]
theorem complex.of_real_zero  :
↑0 = 0
source
@[simp]
theorem complex.of_real_eq_zero {z : ℝ} :
↑z = 0 ↔ z = 0
source
theorem complex.of_real_ne_zero {z : ℝ} :
↑z ≠ 0 ↔ z ≠ 0
source
@[protected, instance]
def complex.has_one  :
has_one ℂ
Equations
source
@[simp]
theorem complex.one_re  :
1.re = 1
source
@[simp]
theorem complex.one_im  :
1.im = 0
source
@[simp, norm_cast]
theorem complex.of_real_one  :
↑1 = 1
source
@[simp]
theorem complex.of_real_eq_one {z : ℝ} :
↑z = 1 ↔ z = 1
source
theorem complex.of_real_ne_one {z : ℝ} :
↑z ≠ 1 ↔ z ≠ 1
source
@[protected, instance]
def complex.has_add  :
has_add ℂ
Equations
source
@[simp]
theorem complex.add_re (z w : ℂ) :
(z + w).re = z.re + w.re
source
@[simp]
theorem complex.add_im (z w : ℂ) :
(z + w).im = z.im + w.im
source
@[simp]
theorem complex.bit0_re (z : ℂ) :
(bit0 z).re = bit0 z.re
source
@[simp]
theorem complex.bit1_re (z : ℂ) :
(bit1 z).re = bit1 z.re
source
@[simp]
theorem complex.bit0_im (z : ℂ) :
(bit0 z).im = bit0 z.im
source
@[simp]
theorem complex.bit1_im (z : ℂ) :
(bit1 z).im = bit0 z.im
source
@[simp, norm_cast]
theorem complex.of_real_add (r s : ℝ) :
↑(r + s) = ↑r + ↑s
source
@[simp, norm_cast]
theorem complex.of_real_bit0 (r : ℝ) :
↑(bit0 r) = bit0 ↑r
source
@[simp, norm_cast]
theorem complex.of_real_bit1 (r : ℝ) :
↑(bit1 r) = bit1 ↑r
source
@[protected, instance]
def complex.has_neg  :
has_neg ℂ
Equations
source
@[simp]
theorem complex.neg_re (z : ℂ) :
(-z).re = -z.re
source
@[simp]
theorem complex.neg_im (z : ℂ) :
(-z).im = -z.im
source
@[simp, norm_cast]
theorem complex.of_real_neg (r : ℝ) :
↑-r = -↑r
source
@[protected, instance]
def complex.has_sub  :
has_sub ℂ
Equations
source
@[protected, instance]
def complex.has_mul  :
has_mul ℂ
Equations
source
@[simp]
theorem complex.mul_re (z w : ℂ) :
(z * w).re = (z.re) * w.re - (z.im) * w.im
source
@[simp]
theorem complex.mul_im (z w : ℂ) :
(z * w).im = (z.re) * w.im + (z.im) * w.re
source
@[simp, norm_cast]
theorem complex.of_real_mul (r s : ℝ) :
↑r * s = (↑r) * ↑s
source
theorem complex.of_real_mul_re (r : ℝ) (z : ℂ) :
((↑r) * z).re = r * z.re
source
theorem complex.of_real_mul_im (r : ℝ) (z : ℂ) :
((↑r) * z).im = r * z.im
source
theorem complex.of_real_mul' (r : ℝ) (z : ℂ) :
(↑r) * z = {re := r * z.re, im := r * z.im}

The imaginary unit, I #

source
def complex.I  :
ℂ

The imaginary unit.

Equations
source
@[simp]
theorem complex.I_re  :
complex.I.re = 0
source
@[simp]
theorem complex.I_im  :
complex.I.im = 1
source
@[simp]
theorem complex.I_mul_I  :
complex.I * complex.I = -1
source
theorem complex.I_mul (z : ℂ) :
complex.I * z = {re := -z.im, im := z.re}
source
theorem complex.I_ne_zero  :
complex.I ≠ 0
source
theorem complex.mk_eq_add_mul_I (a b : ℝ) :
{re := a, im := b} = ↑a + (↑b) * complex.I
source
@[simp]
theorem complex.re_add_im (z : ℂ) :
↑(z.re) + (↑(z.im)) * complex.I = z
source
theorem complex.mul_I_re (z : ℂ) :
(z * complex.I).re = -z.im
source
theorem complex.mul_I_im (z : ℂ) :
(z * complex.I).im = z.re
source
theorem complex.I_mul_re (z : ℂ) :
(complex.I * z).re = -z.im
source
theorem complex.I_mul_im (z : ℂ) :
(complex.I * z).im = z.re

Commutative ring instance and lemmas #

source
@[protected, instance]
def complex.comm_ring  :
comm_ring ℂ
Equations
source
@[protected, instance]
def complex.ring  :
ring ℂ

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

Equations
source
def complex.re_add_group_hom  :
ℂ →+ ℝ

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

Equations
source
@[simp]
theorem complex.coe_re_add_group_hom  :
⇑complex.re_add_group_hom = complex.re
source
def complex.im_add_group_hom  :
ℂ →+ ℝ

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

Equations
source
@[simp]
theorem complex.coe_im_add_group_hom  :
⇑complex.im_add_group_hom = complex.im
source
@[simp]
theorem complex.I_pow_bit0 (n : ℕ) :
complex.I ^ bit0 n = (-1) ^ n
source
@[simp]
theorem complex.I_pow_bit1 (n : ℕ) :
complex.I ^ bit1 n = ((-1) ^ n) * complex.I

Complex conjugation #

source
@[protected, instance]
def complex.star_ring  :
star_ring ℂ

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
source
@[simp]
theorem complex.conj_re (z : ℂ) :
(⇑conj z).re = z.re
source
@[simp]
theorem complex.conj_im (z : ℂ) :
(⇑conj z).im = -z.im
source
theorem complex.conj_of_real (r : ℝ) :
⇑conj ↑r = ↑r
source
@[simp]
theorem complex.conj_I  :
⇑conj complex.I = -complex.I
source
theorem complex.conj_bit0 (z : ℂ) :
⇑conj (bit0 z) = bit0 (⇑conj z)
source
theorem complex.conj_bit1 (z : ℂ) :
⇑conj (bit1 z) = bit1 (⇑conj z)
source
@[simp]
theorem complex.conj_neg_I  :
⇑conj (-complex.I) = complex.I
source
theorem complex.eq_conj_iff_real {z : ℂ} :
⇑conj z = z ↔ ∃ (r : ℝ), z = ↑r
source
theorem complex.eq_conj_iff_re {z : ℂ} :
⇑conj z = z ↔ ↑(z.re) = z
source
theorem complex.eq_conj_iff_im {z : ℂ} :
⇑conj z = z ↔ z.im = 0
source
@[simp, nolint]
theorem complex.star_def  :
star = ⇑conj

Norm squared #

source
def complex.norm_sq  :
ℂ →*₀ ℝ

The norm squared function.

Equations
source
theorem complex.norm_sq_apply (z : ℂ) :
⇑complex.norm_sq z = (z.re) * z.re + (z.im) * z.im
source
@[simp]
theorem complex.norm_sq_of_real (r : ℝ) :
⇑complex.norm_sq ↑r = r * r
source
@[simp]
theorem complex.norm_sq_mk (x y : ℝ) :
⇑complex.norm_sq {re := x, im := y} = x * x + y * y
source
theorem complex.norm_sq_add_mul_I (x y : ℝ) :
⇑complex.norm_sq (↑x + (↑y) * complex.I) = x ^ 2 + y ^ 2
source
theorem complex.norm_sq_eq_conj_mul_self {z : ℂ} :
↑(⇑complex.norm_sq z) = (⇑conj z) * z
source
@[simp]
theorem complex.norm_sq_zero  :
⇑complex.norm_sq 0 = 0
source
@[simp]
theorem complex.norm_sq_one  :
⇑complex.norm_sq 1 = 1
source
@[simp]
theorem complex.norm_sq_I  :
⇑complex.norm_sq complex.I = 1
source
theorem complex.norm_sq_nonneg (z : ℂ) :
0 ≤ ⇑complex.norm_sq z
source
theorem complex.norm_sq_eq_zero {z : ℂ} :
⇑complex.norm_sq z = 0 ↔ z = 0
source
@[simp]
theorem complex.norm_sq_pos {z : ℂ} :
0 < ⇑complex.norm_sq z ↔ z ≠ 0
source
@[simp]
theorem complex.norm_sq_neg (z : ℂ) :
⇑complex.norm_sq (-z) = ⇑complex.norm_sq z
source
@[simp]
theorem complex.norm_sq_conj (z : ℂ) :
⇑complex.norm_sq (⇑conj z) = ⇑complex.norm_sq z
source
theorem complex.norm_sq_mul (z w : ℂ) :
⇑complex.norm_sq (z * w) = (⇑complex.norm_sq z) * ⇑complex.norm_sq w
source
theorem complex.norm_sq_add (z w : ℂ) :
⇑complex.norm_sq (z + w) = ⇑complex.norm_sq z + ⇑complex.norm_sq w + 2 * (z * ⇑conj w).re
source
theorem complex.re_sq_le_norm_sq (z : ℂ) :
(z.re) * z.re ≤ ⇑complex.norm_sq z
source
theorem complex.im_sq_le_norm_sq (z : ℂ) :
(z.im) * z.im ≤ ⇑complex.norm_sq z
source
theorem complex.mul_conj (z : ℂ) :
z * ⇑conj z = ↑(⇑complex.norm_sq z)
source
theorem complex.add_conj (z : ℂ) :
z + ⇑conj z = ↑2 * z.re
source
def complex.of_real  :
ℝ →+* ℂ

The coercion ℝ → ℂ as a ring_hom.

Equations
source
@[simp]
theorem complex.of_real_eq_coe (r : ℝ) :
⇑complex.of_real r = ↑r
source
@[simp]
theorem complex.I_sq  :
complex.I ^ 2 = -1
source
@[simp]
theorem complex.sub_re (z w : ℂ) :
(z - w).re = z.re - w.re
source
@[simp]
theorem complex.sub_im (z w : ℂ) :
(z - w).im = z.im - w.im
source
@[simp, norm_cast]
theorem complex.of_real_sub (r s : ℝ) :
↑(r - s) = ↑r - ↑s
source
@[simp, norm_cast]
theorem complex.of_real_pow (r : ℝ) (n : ℕ) :
↑(r ^ n) = ↑r ^ n
source
theorem complex.sub_conj (z : ℂ) :
z - ⇑conj z = (↑2 * z.im) * complex.I
source
theorem complex.norm_sq_sub (z w : ℂ) :
⇑complex.norm_sq (z - w) = ⇑complex.norm_sq z + ⇑complex.norm_sq w - 2 * (z * ⇑conj w).re

Inversion #

source
@[protected, instance]
noncomputable def complex.has_inv  :
has_inv ℂ
Equations
source
theorem complex.inv_def (z : ℂ) :
z⁻¹ = (⇑conj z) * ↑(⇑complex.norm_sq z)⁻¹
source
@[simp]
theorem complex.inv_re (z : ℂ) :
z⁻¹.re = z.re / ⇑complex.norm_sq z
source
@[simp]
theorem complex.inv_im (z : ℂ) :
z⁻¹.im = -z.im / ⇑complex.norm_sq z
source
@[simp, norm_cast]
theorem complex.of_real_inv (r : ℝ) :
↑r⁻¹ = (↑r)⁻¹
source
@[protected]
theorem complex.inv_zero  :
0⁻¹ = 0
source
@[protected]
theorem complex.mul_inv_cancel {z : ℂ} (h : z ≠ 0) :
z * z⁻¹ = 1

Field instance and lemmas #

source
@[protected, instance]
noncomputable def complex.field  :
field ℂ
Equations
source
@[simp]
theorem complex.I_zpow_bit0 (n : ℤ) :
complex.I ^ bit0 n = (-1) ^ n
source
@[simp]
theorem complex.I_zpow_bit1 (n : ℤ) :
complex.I ^ bit1 n = ((-1) ^ n) * complex.I
source
theorem complex.div_re (z w : ℂ) :
(z / w).re = (z.re) * w.re / ⇑complex.norm_sq w + (z.im) * w.im / ⇑complex.norm_sq w
source
theorem complex.div_im (z w : ℂ) :
(z / w).im = (z.im) * w.re / ⇑complex.norm_sq w - (z.re) * w.im / ⇑complex.norm_sq w
source
theorem complex.conj_inv (x : ℂ) :
⇑conj x⁻¹ = (⇑conj x)⁻¹
source
@[simp, norm_cast]
theorem complex.of_real_div (r s : ℝ) :
↑(r / s) = ↑r / ↑s
source
@[simp, norm_cast]
theorem complex.of_real_zpow (r : ℝ) (n : ℤ) :
↑(r ^ n) = ↑r ^ n
source
@[simp]
theorem complex.div_I (z : ℂ) :
z / complex.I = -z * complex.I
source
@[simp]
theorem complex.inv_I  :
complex.I⁻¹ = -complex.I
source
@[simp]
theorem complex.norm_sq_inv (z : ℂ) :
⇑complex.norm_sq z⁻¹ = (⇑complex.norm_sq z)⁻¹
source
@[simp]
theorem complex.norm_sq_div (z w : ℂ) :
⇑complex.norm_sq (z / w) = ⇑complex.norm_sq z / ⇑complex.norm_sq w

Cast lemmas #

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

Characteristic zero #

source
@[protected, instance]
def complex.char_zero_complex  :
char_zero ℂ
source
theorem complex.re_eq_add_conj (z : ℂ) :
↑(z.re) = (z + ⇑conj z) / 2

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

source
theorem complex.im_eq_sub_conj (z : ℂ) :
↑(z.im) = (z - ⇑conj z) / 2 * complex.I

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

Absolute value #

source
noncomputable def complex.abs (z : ℂ) :
ℝ

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

Equations
source
@[simp, norm_cast]
theorem complex.abs_of_real (r : ℝ) :
complex.abs ↑r = |r|
source
theorem complex.abs_of_nonneg {r : ℝ} (h : 0 ≤ r) :
complex.abs ↑r = r
source
theorem complex.abs_of_nat (n : ℕ) :
complex.abs ↑n = ↑n
source
theorem complex.mul_self_abs (z : ℂ) :
(complex.abs z) * complex.abs z = ⇑complex.norm_sq z
source
theorem complex.sq_abs (z : ℂ) :
complex.abs z ^ 2 = ⇑complex.norm_sq z
source
@[simp]
theorem complex.sq_abs_sub_sq_re (z : ℂ) :
complex.abs z ^ 2 - z.re ^ 2 = z.im ^ 2
source
@[simp]
theorem complex.sq_abs_sub_sq_im (z : ℂ) :
complex.abs z ^ 2 - z.im ^ 2 = z.re ^ 2
source
@[simp]
theorem complex.abs_zero  :
complex.abs 0 = 0
source
@[simp]
theorem complex.abs_one  :
complex.abs 1 = 1
source
@[simp]
theorem complex.abs_I  :
complex.abs complex.I = 1
source
@[simp]
theorem complex.abs_two  :
complex.abs 2 = 2
source
theorem complex.abs_nonneg (z : ℂ) :
0 ≤ complex.abs z
source
@[simp]
theorem complex.abs_eq_zero {z : ℂ} :
complex.abs z = 0 ↔ z = 0
source
theorem complex.abs_ne_zero {z : ℂ} :
complex.abs z ≠ 0 ↔ z ≠ 0
source
@[simp]
theorem complex.abs_conj (z : ℂ) :
complex.abs (⇑conj z) = complex.abs z
source
@[simp]
theorem complex.abs_mul (z w : ℂ) :
complex.abs (z * w) = (complex.abs z) * complex.abs w
source
@[simp]
theorem complex.abs_hom_apply (z : ℂ) :
⇑complex.abs_hom z = complex.abs z
source
noncomputable def complex.abs_hom  :
ℂ →*₀ ℝ

complex.abs as a monoid_with_zero_hom.

Equations
source
@[simp]
theorem complex.abs_prod {ι : Type u_1} (s : finset ι) (f : ι → ℂ) :
complex.abs (s.prod f) = ∏ (i : ι) in s, complex.abs (f i)
source
@[simp]
theorem complex.abs_pow (z : ℂ) (n : ℕ) :
complex.abs (z ^ n) = complex.abs z ^ n
source
@[simp]
theorem complex.abs_zpow (z : ℂ) (n : ℤ) :
complex.abs (z ^ n) = complex.abs z ^ n
source
theorem complex.abs_re_le_abs (z : ℂ) :
|z.re| ≤ complex.abs z
source
theorem complex.abs_im_le_abs (z : ℂ) :
|z.im| ≤ complex.abs z
source
theorem complex.re_le_abs (z : ℂ) :
z.re ≤ complex.abs z
source
theorem complex.im_le_abs (z : ℂ) :
z.im ≤ complex.abs z
source
@[simp]
theorem complex.abs_re_lt_abs {z : ℂ} :
|z.re| < complex.abs z ↔ z.im ≠ 0
source
@[simp]
theorem complex.abs_im_lt_abs {z : ℂ} :
|z.im| < complex.abs z ↔ z.re ≠ 0
source
theorem complex.abs_add (z w : ℂ) :
complex.abs (z + w) ≤ complex.abs z + complex.abs w

The triangle inequality for complex numbers.

source
@[protected, instance]
def complex.abs.is_absolute_value  :
is_absolute_value complex.abs
source
@[simp]
theorem complex.abs_abs (z : ℂ) :
|complex.abs z| = complex.abs z
source
@[simp]
theorem complex.abs_pos {z : ℂ} :
0 < complex.abs z ↔ z ≠ 0
source
@[simp]
theorem complex.abs_neg (z : ℂ) :
complex.abs (-z) = complex.abs z
source
theorem complex.abs_sub_comm (z w : ℂ) :
complex.abs (z - w) = complex.abs (w - z)
source
theorem complex.abs_sub_le (a b c : ℂ) :
complex.abs (a - c) ≤ complex.abs (a - b) + complex.abs (b - c)
source
@[simp]
theorem complex.abs_inv (z : ℂ) :
complex.abs z⁻¹ = (complex.abs z)⁻¹
source
@[simp]
theorem complex.abs_div (z w : ℂ) :
complex.abs (z / w) = complex.abs z / complex.abs w
source
theorem complex.abs_abs_sub_le_abs_sub (z w : ℂ) :
|complex.abs z - complex.abs w| ≤ complex.abs (z - w)
source
theorem complex.abs_le_abs_re_add_abs_im (z : ℂ) :
complex.abs z ≤ |z.re| + |z.im|
source
theorem complex.abs_re_div_abs_le_one (z : ℂ) :
|z.re / complex.abs z| ≤ 1
source
theorem complex.abs_im_div_abs_le_one (z : ℂ) :
|z.im / complex.abs z| ≤ 1
source
@[simp, norm_cast]
theorem complex.abs_cast_nat (n : ℕ) :
complex.abs ↑n = ↑n
source
@[simp, norm_cast]
theorem complex.int_cast_abs (n : ℤ) :
↑|n| = complex.abs ↑n
source
theorem complex.norm_sq_eq_abs (x : ℂ) :
⇑complex.norm_sq x = complex.abs x ^ 2
source
@[protected, instance]
def complex.partial_order  :
partial_order ℂ

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
source
theorem complex.le_def {z w : ℂ} :
z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im
source
theorem complex.lt_def {z w : ℂ} :
z < w ↔ z.re < w.re ∧ z.im = w.im
source
@[simp, norm_cast]
theorem complex.real_le_real {x y : ℝ} :
↑x ≤ ↑y ↔ x ≤ y
source
@[simp, norm_cast]
theorem complex.real_lt_real {x y : ℝ} :
↑x < ↑y ↔ x < y
source
@[simp, norm_cast]
theorem complex.zero_le_real {x : ℝ} :
0 ≤ ↑x ↔ 0 ≤ x
source
@[simp, norm_cast]
theorem complex.zero_lt_real {x : ℝ} :
0 < ↑x ↔ 0 < x
source
theorem complex.not_le_iff {z w : ℂ} :
¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im
source
theorem complex.not_lt_iff {z w : ℂ} :
¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im
source
theorem complex.not_le_zero_iff {z : ℂ} :
¬z ≤ 0 ↔ 0 < z.re ∨ z.im ≠ 0
source
theorem complex.not_lt_zero_iff {z : ℂ} :
¬z < 0 ↔ 0 ≤ z.re ∨ z.im ≠ 0
source
@[protected, instance]
def complex.ordered_comm_ring  :
ordered_comm_ring ℂ

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

Equations
source
@[protected, instance]
def complex.star_ordered_ring  :
star_ordered_ring ℂ

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 #

source
theorem complex.is_cau_seq_re (f : cau_seq ℂ complex.abs) :
is_cau_seq abs (λ (n : ℕ), (⇑f n).re)
source
theorem complex.is_cau_seq_im (f : cau_seq ℂ complex.abs) :
is_cau_seq abs (λ (n : ℕ), (⇑f n).im)
source
noncomputable def complex.cau_seq_re (f : cau_seq ℂ complex.abs) :
cau_seq ℝ abs

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

Equations
source
noncomputable def complex.cau_seq_im (f : cau_seq ℂ complex.abs) :
cau_seq ℝ abs

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

Equations
source
theorem complex.is_cau_seq_abs {f : ℕ → ℂ} (hf : is_cau_seq complex.abs f) :
is_cau_seq abs (complex.abs ∘ f)
source
noncomputable def complex.lim_aux (f : cau_seq ℂ complex.abs) :
ℂ

The limit of a Cauchy sequence of complex numbers.

Equations
source
theorem complex.equiv_lim_aux (f : cau_seq ℂ complex.abs) :
f ≈ cau_seq.const complex.abs (complex.lim_aux f)
source
@[protected, instance]
def complex.abs.cau_seq.is_complete  :
cau_seq.is_complete ℂ complex.abs
source
theorem complex.lim_eq_lim_im_add_lim_re (f : cau_seq ℂ complex.abs) :
f.lim = ↑((complex.cau_seq_re f).lim) + (↑((complex.cau_seq_im f).lim)) * complex.I
source
theorem complex.lim_re (f : cau_seq ℂ complex.abs) :
(complex.cau_seq_re f).lim = f.lim.re
source
theorem complex.lim_im (f : cau_seq ℂ complex.abs) :
(complex.cau_seq_im f).lim = f.lim.im
source
theorem complex.is_cau_seq_conj (f : cau_seq ℂ complex.abs) :
is_cau_seq complex.abs (λ (n : ℕ), ⇑conj (⇑f n))
source
noncomputable def complex.cau_seq_conj (f : cau_seq ℂ complex.abs) :
cau_seq ℂ complex.abs

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

Equations
source
theorem complex.lim_conj (f : cau_seq ℂ complex.abs) :
(complex.cau_seq_conj f).lim = ⇑conj f.lim
source
noncomputable def complex.cau_seq_abs (f : cau_seq ℂ complex.abs) :
cau_seq ℝ abs

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

Equations
source
theorem complex.lim_abs (f : cau_seq ℂ complex.abs) :
(complex.cau_seq_abs f).lim = complex.abs f.lim
source
@[simp, norm_cast]
theorem complex.of_real_prod {α : Type u_1} (s : finset α) (f : α → ℝ) :
↑∏ (i : α) in s, f i = ∏ (i : α) in s, ↑(f i)
source
@[simp, norm_cast]
theorem complex.of_real_sum {α : Type u_1} (s : finset α) (f : α → ℝ) :
↑∑ (i : α) in s, f i = ∑ (i : α) in s, ↑(f i)