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. For the result that the complex numbers are algebraically closed, see Complex.isAlgClosed in Mathlib.Analysis.Complex.Polynomial.Basic.

Definition and basic arithmetic #

structure Complex :

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

re : ℝ
The real part of a complex number.
im : ℝ
The imaginary part of a complex number.

Instances For

Lean.ParserDescr

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

Instances For

@[implicit_reducible]

noncomputable instance Complex.instDecidableEq :

DecidableEq ℂ

def Complex.equivRealProd :

ℂ ≃ ℝ × ℝ

The equivalence between the complex numbers and ℝ × ℝ.

Instances For

@[simp]

theorem Complex.equivRealProd_apply (z : ℂ) :

equivRealProd z = (z.re, z.im)

@[simp]

theorem Complex.eta (z : ℂ) :

{ re := z.re, im := z.im } = z

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

theorem Complex.forall {p : ℂ → Prop} :

(∀ (x : ℂ), p x) ↔ ∀ (a b : ℝ), p { re := a, im := b }

theorem Complex.exists {p : ℂ → Prop} :

(∃ (x : ℂ), p x) ↔ ∃ (a : ℝ) (b : ℝ), p { re := a, im := b }

theorem Complex.re_surjective :

Function.Surjective re

theorem Complex.im_surjective :

Function.Surjective im

@[simp]

theorem Complex.range_re :

Set.range re = Set.univ

@[simp]

theorem Complex.range_im :

Set.range im = Set.univ

def Complex.ofReal (r : ℝ) :

The natural inclusion of the real numbers into the complex numbers.

Instances For

@[implicit_reducible]

instance Complex.instCoeReal :

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

theorem Complex.ofReal_injective :

Function.Injective ofReal

instance Complex.canLift :

CanLift ℂ ℝ ofReal fun (z : ℂ) => z.im = 0

def Complex.reProdIm (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.

Instances For

def Complex.«term_×ℂ_» :

Lean.TrailingParserDescr

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

theorem Complex.mem_reProdIm {z : ℂ} {s t : Set ℝ} :

z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t

@[implicit_reducible]

instance Complex.instZero :

@[implicit_reducible]

instance Complex.instInhabited :

@[simp]

theorem Complex.zero_re :

re 0 = 0

@[simp]

theorem Complex.zero_im :

im 0 = 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

@[implicit_reducible]

instance Complex.instOne :

@[simp]

theorem Complex.one_re :

re 1 = 1

@[simp]

theorem Complex.one_im :

im 1 = 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

@[implicit_reducible]

instance Complex.instAdd :

@[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.ofReal_add (r s : ℝ) :

↑(r + s) = ↑r + ↑s

@[implicit_reducible]

instance Complex.instNeg :

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

@[implicit_reducible]

instance Complex.instSub :

@[implicit_reducible]

instance Complex.instMul :

@[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.re_ofReal_mul (r : ℝ) (z : ℂ) :

(↑r * z).re = r * z.re

theorem Complex.im_ofReal_mul (r : ℝ) (z : ℂ) :

(↑r * z).im = r * z.im

theorem Complex.re_mul_ofReal (z : ℂ) (r : ℝ) :

(z * ↑r).re = z.re * r

theorem Complex.im_mul_ofReal (z : ℂ) (r : ℝ) :

(z * ↑r).im = z.im * r

theorem Complex.ofReal_mul' (r : ℝ) (z : ℂ) :

↑r * z = { re := r * z.re, im := r * z.im }

The imaginary unit, `I` #

def Complex.I :

The imaginary unit.

Instances For

@[simp]

theorem Complex.I_re :

I.re = 0

@[simp]

theorem Complex.I_im :

I.im = 1

@[simp]

theorem Complex.I_mul_I :

I * I = -1

theorem Complex.I_mul (z : ℂ) :

I * z = { re := -z.im, im := z.re }

@[simp]

theorem Complex.I_ne_zero :

theorem Complex.mk_eq_add_mul_I (a b : ℝ) :

{ re := a, im := b } = ↑a + ↑b * I

@[simp]

theorem Complex.re_add_im (z : ℂ) :

↑z.re + ↑z.im * I = z

theorem Complex.mul_I_re (z : ℂ) :

(z * I).re = -z.im

theorem Complex.mul_I_im (z : ℂ) :

(z * I).im = z.re

theorem Complex.I_mul_re (z : ℂ) :

(I * z).re = -z.im

theorem Complex.I_mul_im (z : ℂ) :

(I * z).im = z.re

@[simp]

theorem Complex.equivRealProd_symm_apply (p : ℝ × ℝ) :

equivRealProd.symm p = ↑p.1 + ↑p.2 * I

def Complex.equivRealProdAddHom :

ℂ ≃+ ℝ × ℝ

The natural AddEquiv from ℂ to ℝ × ℝ.

Instances For

@[simp]

theorem Complex.equivRealProdAddHom_symm_apply_re (p : ℝ × ℝ) :

(equivRealProdAddHom.symm p).re = p.1

@[simp]

theorem Complex.equivRealProdAddHom_symm_apply_im (p : ℝ × ℝ) :

(equivRealProdAddHom.symm p).im = p.2

@[simp]

theorem Complex.equivRealProdAddHom_apply (z : ℂ) :

equivRealProdAddHom z = (z.re, z.im)

theorem Complex.equivRealProdAddHom_symm_apply (p : ℝ × ℝ) :

equivRealProdAddHom.symm p = ↑p.1 + ↑p.2 * I

Commutative ring instance and lemmas #

instance Complex.instNontrivial :

@[implicit_reducible]

def Complex.SMul.instSMulRealComplex {R : Type u_1} [SMul R ℝ] :

Scalar multiplication by R on ℝ extends to ℂ. This is used here and in Mathlib/LinearAlgebra/Complex/Module.lean to transfer instances from ℝ to ℂ, but is not needed outside, so we make it scoped.

Instances For

theorem Complex.smul_re {R : Type u_1} [SMul R ℝ] (r : R) (z : ℂ) :

(r • z).re = r • z.re

theorem Complex.smul_im {R : Type u_1} [SMul R ℝ] (r : R) (z : ℂ) :

(r • z).im = r • z.im

@[simp]

theorem Complex.real_smul {x : ℝ} {z : ℂ} :

x • z = ↑x * z

@[implicit_reducible]

instance Complex.addCommGroup :

AddCommGroup ℂ

Casts #

@[implicit_reducible]

instance Complex.instNatCast :

@[implicit_reducible]

instance Complex.instIntCast :

@[implicit_reducible]

instance Complex.instNNRatCast :

@[implicit_reducible]

instance Complex.instRatCast :

@[simp]

theorem Complex.ofReal_ofNat (n : ℕ) [n.AtLeastTwo] :

↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Complex.ofReal_natCast (n : ℕ) :

↑↑n = ↑n

@[simp]

theorem Complex.ofReal_intCast (n : ℤ) :

↑↑n = ↑n

@[simp]

theorem Complex.ofReal_nnratCast (q : ℚ≥0) :

↑↑q = ↑q

@[simp]

theorem Complex.ofReal_ratCast (q : ℚ) :

↑↑q = ↑q

@[simp]

theorem Complex.re_ofNat (n : ℕ) [n.AtLeastTwo] :

(OfNat.ofNat n).re = OfNat.ofNat n

@[simp]

theorem Complex.im_ofNat (n : ℕ) [n.AtLeastTwo] :

(OfNat.ofNat n).im = 0

@[simp]

theorem Complex.natCast_re (n : ℕ) :

(↑n).re = ↑n

@[simp]

theorem Complex.natCast_im (n : ℕ) :

(↑n).im = 0

@[simp]

theorem Complex.intCast_re (n : ℤ) :

(↑n).re = ↑n

@[simp]

theorem Complex.intCast_im (n : ℤ) :

(↑n).im = 0

@[simp]

theorem Complex.re_nnratCast (q : ℚ≥0) :

(↑q).re = ↑q

@[simp]

theorem Complex.im_nnratCast (q : ℚ≥0) :

(↑q).im = 0

@[simp]

theorem Complex.ratCast_re (q : ℚ) :

(↑q).re = ↑q

@[simp]

theorem Complex.ratCast_im (q : ℚ) :

(↑q).im = 0

Ring structure #

@[implicit_reducible]

instance Complex.addGroupWithOne :

AddGroupWithOne ℂ

@[implicit_reducible]

instance Complex.commRing :

@[implicit_reducible]

instance Complex.instRing :

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

@[implicit_reducible]

instance Complex.instCommSemiring :

CommSemiring ℂ

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

@[implicit_reducible]

instance Complex.instSemiring :

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

def Complex.reAddGroupHom :

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

Instances For

@[simp]

theorem Complex.coe_reAddGroupHom :

⇑reAddGroupHom = re

def Complex.imAddGroupHom :

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

Instances For

@[simp]

theorem Complex.coe_imAddGroupHom :

⇑imAddGroupHom = im

theorem Complex.re_nsmul (n : ℕ) (z : ℂ) :

(n • z).re = n • z.re

theorem Complex.im_nsmul (n : ℕ) (z : ℂ) :

(n • z).im = n • z.im

theorem Complex.re_zsmul (n : ℤ) (z : ℂ) :

(n • z).re = n • z.re

theorem Complex.im_zsmul (n : ℤ) (z : ℂ) :

(n • z).im = n • z.im

@[simp]

theorem Complex.re_nnqsmul (q : ℚ≥0) (z : ℂ) :

(q • z).re = q • z.re

@[simp]

theorem Complex.im_nnqsmul (q : ℚ≥0) (z : ℂ) :

(q • z).im = q • z.im

@[simp]

theorem Complex.re_qsmul (q : ℚ) (z : ℂ) :

(q • z).re = q • z.re

@[simp]

theorem Complex.im_qsmul (q : ℚ) (z : ℂ) :

(q • z).im = q • z.im

theorem Complex.ofReal_nsmul (n : ℕ) (r : ℝ) :

↑(n • r) = n • ↑r

theorem Complex.ofReal_zsmul (n : ℤ) (r : ℝ) :

↑(n • r) = n • ↑r

Complex conjugation #

@[implicit_reducible]

instance Complex.instStarRing :

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 scope ComplexConjugate.

@[simp]

theorem Complex.conj_re (z : ℂ) :

((starRingEnd ℂ) z).re = z.re

@[simp]

theorem Complex.conj_im (z : ℂ) :

((starRingEnd ℂ) z).im = -z.im

@[simp]

theorem Complex.conj_ofReal (r : ℝ) :

(starRingEnd ℂ) ↑r = ↑r

@[simp]

theorem Complex.conj_I :

(starRingEnd ℂ) I = -I

theorem Complex.conj_natCast (n : ℕ) :

(starRingEnd ℂ) ↑n = ↑n

theorem Complex.conj_ofNat (n : ℕ) [n.AtLeastTwo] :

(starRingEnd ℂ) (OfNat.ofNat n) = OfNat.ofNat n

theorem Complex.conj_neg_I :

(starRingEnd ℂ) (-I) = I

theorem Complex.conj_eq_iff_real {z : ℂ} :

(starRingEnd ℂ) z = z ↔ ∃ (r : ℝ), z = ↑r

theorem Complex.conj_eq_iff_re {z : ℂ} :

(starRingEnd ℂ) z = z ↔ ↑z.re = z

theorem Complex.conj_eq_iff_im {z : ℂ} :

(starRingEnd ℂ) z = z ↔ z.im = 0

@[simp]

theorem Complex.star_def :

star = ⇑(starRingEnd ℂ)

Norm squared #

def Complex.normSq :

ℂ →*₀ ℝ

The norm squared function.

Instances For

theorem Complex.normSq_apply (z : ℂ) :

normSq z = z.re * z.re + z.im * z.im

@[simp]

theorem Complex.normSq_ofReal (r : ℝ) :

normSq ↑r = r * r

@[simp]

theorem Complex.normSq_natCast (n : ℕ) :

normSq ↑n = ↑n * ↑n

@[simp]

theorem Complex.normSq_intCast (z : ℤ) :

normSq ↑z = ↑z * ↑z

@[simp]

theorem Complex.normSq_ratCast (q : ℚ) :

normSq ↑q = ↑q * ↑q

@[simp]

theorem Complex.normSq_ofNat (n : ℕ) [n.AtLeastTwo] :

normSq (OfNat.ofNat n) = OfNat.ofNat n * OfNat.ofNat n

@[simp]

theorem Complex.normSq_mk (x y : ℝ) :

normSq { re := x, im := y } = x * x + y * y

theorem Complex.normSq_add_mul_I (x y : ℝ) :

normSq (↑x + ↑y * I) = x ^ 2 + y ^ 2

theorem Complex.normSq_eq_conj_mul_self {z : ℂ} :

↑(normSq z) = (starRingEnd ℂ) z * z

theorem Complex.normSq_zero :

theorem Complex.normSq_one :

@[simp]

theorem Complex.normSq_I :

theorem Complex.normSq_nonneg (z : ℂ) :

theorem Complex.normSq_eq_zero {z : ℂ} :

normSq z = 0 ↔ z = 0

@[simp]

theorem Complex.normSq_pos {z : ℂ} :

0 < normSq z ↔ z ≠ 0

@[simp]

theorem Complex.normSq_neg (z : ℂ) :

normSq (-z) = normSq z

@[simp]

theorem Complex.normSq_conj (z : ℂ) :

normSq ((starRingEnd ℂ) z) = normSq z

theorem Complex.normSq_mul (z w : ℂ) :

normSq (z * w) = normSq z * normSq w

theorem Complex.normSq_add (z w : ℂ) :

normSq (z + w) = normSq z + normSq w + 2 * (z * (starRingEnd ℂ) w).re

theorem Complex.re_sq_le_normSq (z : ℂ) :

z.re * z.re ≤ normSq z

theorem Complex.im_sq_le_normSq (z : ℂ) :

z.im * z.im ≤ normSq z

theorem Complex.mul_conj (z : ℂ) :

z * (starRingEnd ℂ) z = ↑(normSq z)

theorem Complex.add_conj (z : ℂ) :

z + (starRingEnd ℂ) z = ↑(2 * z.re)

def Complex.ofRealHom :

The coercion ℝ → ℂ as a RingHom.

Instances For

@[simp]

theorem Complex.ofRealHom_eq_coe (r : ℝ) :

ofRealHom r = ↑r

@[simp]

theorem Complex.ofReal_comp_add {α : Type u_1} (f g : α → ℝ) :

ofReal ∘ (f + g) = ofReal ∘ f + ofReal ∘ g

@[simp]

theorem Complex.ofReal_comp_sub {α : Type u_1} (f g : α → ℝ) :

ofReal ∘ (f - g) = ofReal ∘ f - ofReal ∘ g

@[simp]

theorem Complex.ofReal_comp_neg {α : Type u_1} (f : α → ℝ) :

ofReal ∘ (-f) = -ofReal ∘ f

theorem Complex.ofReal_comp_nsmul {α : Type u_1} (n : ℕ) (f : α → ℝ) :

ofReal ∘ (n • f) = n • ofReal ∘ f

theorem Complex.ofReal_comp_zsmul {α : Type u_1} (n : ℤ) (f : α → ℝ) :

ofReal ∘ (n • f) = n • ofReal ∘ f

@[simp]

theorem Complex.ofReal_comp_mul {α : Type u_1} (f g : α → ℝ) :

ofReal ∘ (f * g) = ofReal ∘ f * ofReal ∘ g

@[simp]

theorem Complex.ofReal_comp_pow {α : Type u_1} (f : α → ℝ) (n : ℕ) :

ofReal ∘ (f ^ n) = ofReal ∘ f ^ n

@[simp]

theorem Complex.I_sq :

I ^ 2 = -1

@[simp]

theorem Complex.I_pow_three :

I ^ 3 = -I

@[simp]

theorem Complex.I_pow_four :

I ^ 4 = 1

theorem Complex.I_pow_eq_pow_mod (n : ℕ) :

I ^ n = I ^ (n % 4)

@[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 - (starRingEnd ℂ) z = ↑(2 * z.im) * I

theorem Complex.normSq_sub (z w : ℂ) :

normSq (z - w) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re

Inversion #

@[implicit_reducible]

noncomputable instance Complex.instInv :

theorem Complex.inv_def (z : ℂ) :

z⁻¹ = (starRingEnd ℂ) z * ↑(normSq z)⁻¹

@[simp]

theorem Complex.inv_re (z : ℂ) :

z⁻¹.re = z.re / normSq z

@[simp]

theorem Complex.inv_im (z : ℂ) :

z⁻¹.im = -z.im / normSq z

@[simp]

theorem Complex.ofReal_inv (r : ℝ) :

↑r⁻¹ = (↑r)⁻¹

theorem Complex.inv_zero :

theorem Complex.mul_inv_cancel {z : ℂ} (h : z ≠ 0) :

z * z⁻¹ = 1

@[implicit_reducible]

noncomputable instance Complex.instDivInvMonoid :

DivInvMonoid ℂ

theorem Complex.div_re (z w : ℂ) :

(z / w).re = z.re * w.re / normSq w + z.im * w.im / normSq w

theorem Complex.div_im (z w : ℂ) :

(z / w).im = z.im * w.re / normSq w - z.re * w.im / normSq w

Field instance and lemmas #

@[implicit_reducible]

noncomputable instance Complex.instField :

@[simp]

theorem Complex.ofReal_nnqsmul (q : ℚ≥0) (r : ℝ) :

↑(q • r) = q • ↑r

@[simp]

theorem Complex.ofReal_qsmul (q : ℚ) (r : ℝ) :

↑(q • r) = q • ↑r

theorem Complex.conj_inv (x : ℂ) :

(starRingEnd ℂ) x⁻¹ = ((starRingEnd ℂ) 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 : ℂ) :

z / I = -(z * I)

@[simp]

theorem Complex.inv_I :

theorem Complex.normSq_inv (z : ℂ) :

normSq z⁻¹ = (normSq z)⁻¹

theorem Complex.normSq_div (z w : ℂ) :

normSq (z / w) = normSq z / normSq w

theorem Complex.div_ofReal (z : ℂ) (x : ℝ) :

z / ↑x = { re := z.re / x, im := z.im / x }

theorem Complex.div_natCast (z : ℂ) (n : ℕ) :

z / ↑n = { re := z.re / ↑n, im := z.im / ↑n }

theorem Complex.div_intCast (z : ℂ) (n : ℤ) :

z / ↑n = { re := z.re / ↑n, im := z.im / ↑n }

theorem Complex.div_ratCast (z : ℂ) (x : ℚ) :

z / ↑x = { re := z.re / ↑x, im := z.im / ↑x }

theorem Complex.div_ofNat (z : ℂ) (n : ℕ) [n.AtLeastTwo] :

z / OfNat.ofNat n = { re := z.re / OfNat.ofNat n, im := z.im / OfNat.ofNat n }

@[simp]

theorem Complex.div_ofReal_re (z : ℂ) (x : ℝ) :

(z / ↑x).re = z.re / x

@[simp]

theorem Complex.div_ofReal_im (z : ℂ) (x : ℝ) :

(z / ↑x).im = z.im / x

@[simp]

theorem Complex.div_natCast_re (z : ℂ) (n : ℕ) :

(z / ↑n).re = z.re / ↑n

@[simp]

theorem Complex.div_natCast_im (z : ℂ) (n : ℕ) :

(z / ↑n).im = z.im / ↑n

@[simp]

theorem Complex.div_intCast_re (z : ℂ) (n : ℤ) :

(z / ↑n).re = z.re / ↑n

@[simp]

theorem Complex.div_intCast_im (z : ℂ) (n : ℤ) :

(z / ↑n).im = z.im / ↑n

@[simp]

theorem Complex.div_ratCast_re (z : ℂ) (x : ℚ) :

(z / ↑x).re = z.re / ↑x

@[simp]

theorem Complex.div_ratCast_im (z : ℂ) (x : ℚ) :

(z / ↑x).im = z.im / ↑x

@[simp]

theorem Complex.div_ofNat_re (z : ℂ) (n : ℕ) [n.AtLeastTwo] :

(z / OfNat.ofNat n).re = z.re / OfNat.ofNat n

@[simp]

theorem Complex.div_ofNat_im (z : ℂ) (n : ℕ) [n.AtLeastTwo] :

(z / OfNat.ofNat n).im = z.im / OfNat.ofNat n

Characteristic zero #

instance Complex.instCharZero :

instance Complex.instIsAddTorsionFree :

IsAddTorsionFree ℂ

theorem Complex.re_eq_add_conj (z : ℂ) :

↑z.re = (z + (starRingEnd ℂ) 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 - (starRingEnd ℂ) z) / (2 * I)

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

@[implicit_reducible]

unsafe instance Complex.instRepr :

Show the imaginary number ⟨x, y⟩ as an "x + y*I" string

Note that the Real numbers used for x and y will show as Cauchy sequences due to the way Real numbers are represented.

theorem Complex.preimage_equivRealProd_prod (s t : Set ℝ) :

⇑equivRealProd ⁻¹' s ×ˢ t = s ×ℂ t

The preimage under equivRealProd of s ×ˢ t is s ×ℂ t.

theorem Complex.reProdIm_subset_iff {s s₁ t t₁ : Set ℝ} :

s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

The inequality s × t ⊆ s₁ × t₁ holds in ℂ iff it holds in ℝ × ℝ.

theorem Complex.reProdIm_subset_iff' {s s₁ t t₁ : Set ℝ} :

s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

If s ⊆ s₁ ⊆ ℝ and t ⊆ t₁ ⊆ ℝ, then s × t ⊆ s₁ × t₁ in ℂ.

@[simp]

theorem Complex.reProdIm_nonempty {s t : Set ℝ} :

(s ×ℂ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

theorem Complex.reProdIm_eq_empty {s t : Set ℝ} :

s ×ℂ t = ∅ ↔ s = ∅ ∨ t = ∅

def Complex.Rectangle (z w : ℂ) :

A Rectangle is an axis-parallel rectangle with corners z and w.

Instances For

theorem Complex.horizontalSegment_eq (a₁ a₂ b : ℝ) :

(fun (x : ℝ) => ↑x + ↑b * I) '' Set.uIcc a₁ a₂ = Set.uIcc a₁ a₂ ×ℂ {b}

A real segment [a₁, a₂] translated by b * I is the complex line segment.

theorem Complex.verticalSegment_eq (a b₁ b₂ : ℝ) :

(fun (y : ℝ) => ↑a + ↑y * I) '' Set.uIcc b₁ b₂ = {a} ×ℂ Set.uIcc b₁ b₂

A vertical segment [b₁, b₂] translated by a is the complex line segment.