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 #

source

structure Complex :

Type

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

source

def termℂ :

Lean.ParserDescr

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

Equations

termℂ = Lean.ParserDescr.node `termℂ 1024 (Lean.ParserDescr.symbol "ℂ")

source

noncomputable instance Complex.instDecidableEq :

DecidableEq ℂ

Equations

Complex.instDecidableEq = Classical.decEq ℂ

source

@[simp]

theorem Complex.equivRealProd_apply (z : ℂ) :

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

source

def Complex.equivRealProd :

ℂ ≃ ℝ × ℝ

The equivalence between the complex numbers and ℝ × ℝ.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem Complex.eta (z : ℂ) :

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

source

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

theorem Complex.re_surjective :

Function.Surjective Complex.re

source

theorem Complex.im_surjective :

Function.Surjective Complex.im

source

@[simp]

theorem Complex.range_re :

Set.range Complex.re = Set.univ

source

@[simp]

theorem Complex.range_im :

Set.range Complex.im = Set.univ

source

def Complex.ofReal' (r : ℝ) :

ℂ

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

Equations

↑r = { re := r, im := 0 }

Instances For

Complex.canLift

source

instance Complex.instCoeReal :

Coe ℝ ℂ

Equations

Complex.instCoeReal = { coe := Complex.ofReal' }

source

@[simp]

theorem Complex.ofReal_re (r : ℝ) :

(↑r).re = r

source

@[simp]

theorem Complex.ofReal_im (r : ℝ) :

(↑r).im = 0

source

theorem Complex.ofReal_def (r : ℝ) :

↑r = { re := r, im := 0 }

source

@[simp]

theorem Complex.ofReal_inj {z : ℝ} {w : ℝ} :

↑z = ↑w ↔ z = w

source

theorem Complex.ofReal_injective :

Function.Injective Complex.ofReal'

source

instance Complex.canLift :

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

Equations

Complex.canLift = ⋯

source

def Complex.Set.reProdIm (s : Set ℝ) (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

s ×ℂ t = Complex.re ⁻¹' s ∩ Complex.im ⁻¹' t

source

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.

Equations

Complex.«term_×ℂ_» = Lean.ParserDescr.trailingNode `Complex.term_×ℂ_ 72 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ℂ ") (Lean.ParserDescr.cat `term 73))

source

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

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

source

instance Complex.instZero :

Zero ℂ

Equations

Complex.instZero = { zero := ↑0 }

source

instance Complex.instInhabited :

Inhabited ℂ

Equations

Complex.instInhabited = { default := 0 }

source

@[simp]

theorem Complex.zero_re :

Complex.re 0 = 0

source

@[simp]

theorem Complex.zero_im :

Complex.im 0 = 0

source

@[simp]

theorem Complex.ofReal_zero :

↑0 = 0

source

@[simp]

theorem Complex.ofReal_eq_zero {z : ℝ} :

↑z = 0 ↔ z = 0

source

theorem Complex.ofReal_ne_zero {z : ℝ} :

↑z ≠ 0 ↔ z ≠ 0

source

instance Complex.instOne :

One ℂ

Equations

Complex.instOne = { one := ↑1 }

source

@[simp]

theorem Complex.one_re :

Complex.re 1 = 1

source

@[simp]

theorem Complex.one_im :

Complex.im 1 = 0

source

@[simp]

theorem Complex.ofReal_one :

↑1 = 1

source

@[simp]

theorem Complex.ofReal_eq_one {z : ℝ} :

↑z = 1 ↔ z = 1

source

theorem Complex.ofReal_ne_one {z : ℝ} :

↑z ≠ 1 ↔ z ≠ 1

source

instance Complex.instAdd :

Add ℂ

Equations

Complex.instAdd = { add := fun (z w : ℂ) => { re := z.re + w.re, im := z.im + w.im } }

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

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

source

instance Complex.instNeg :

Neg ℂ

Equations

Complex.instNeg = { neg := fun (z : ℂ) => { re := -z.re, im := -z.im } }

source

@[simp]

theorem Complex.neg_re (z : ℂ) :

(-z).re = -z.re

source

@[simp]

theorem Complex.neg_im (z : ℂ) :

(-z).im = -z.im

source

@[simp]

theorem Complex.ofReal_neg (r : ℝ) :

↑(-r) = -↑r

source

instance Complex.instSub :

Sub ℂ

Equations

Complex.instSub = { sub := fun (z w : ℂ) => { re := z.re - w.re, im := z.im - w.im } }

source

instance Complex.instMul :

Mul ℂ

Equations

Complex.instMul = { mul := fun (z w : ℂ) => { re := z.re * w.re - z.im * w.im, im := z.re * w.im + z.im * w.re } }

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]

theorem Complex.ofReal_mul (r : ℝ) (s : ℝ) :

↑(r * s) = ↑r * ↑s

source

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

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

source

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

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

source

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

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

source

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

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

source

theorem Complex.ofReal_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

Complex.I = { re := 0, im := 1 }

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

@[simp]

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem Complex.equivRealProdAddHom_apply (z : ℂ) :

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

source

def Complex.equivRealProdAddHom :

ℂ ≃+ ℝ × ℝ

The natural AddEquiv from ℂ to ℝ × ℝ.

Equations

Complex.equivRealProdAddHom = { toEquiv := Complex.equivRealProd, map_add' := Complex.equivRealProdAddHom.proof_1 }

source

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

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

Commutative ring instance and lemmas #

source

instance Complex.instNontrivial :

Nontrivial ℂ

Equations

Complex.instNontrivial = ⋯

source

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

SMul R ℂ

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

Equations

Complex.SMul.instSMulRealComplex = { smul := fun (r : R) (x : ℂ) => { re := r • x.re - 0 * x.im, im := r • x.im + 0 * x.re } }

source

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

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

source

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

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

source

@[simp]

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

x • z = ↑x * z

source

instance Complex.addCommGroup :

AddCommGroup ℂ

Equations

Complex.addCommGroup = AddCommGroup.mk Complex.addCommGroup.proof_11

source

instance Complex.addGroupWithOne :

AddGroupWithOne ℂ

Equations

One or more equations did not get rendered due to their size.

source

instance Complex.commRing :

CommRing ℂ

Equations

Complex.commRing = CommRing.mk Complex.commRing.proof_13

source

instance Complex.instRing :

Ring ℂ

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

Equations

Complex.instRing = inferInstance

source

instance Complex.instCommSemiring :

CommSemiring ℂ

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

Equations

Complex.instCommSemiring = inferInstance

source

instance Complex.instSemiring :

Semiring ℂ

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

Equations

Complex.instSemiring = inferInstance

source

def Complex.reAddGroupHom :

ℂ →+ ℝ

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

Equations

Complex.reAddGroupHom = { toFun := Complex.re, map_zero' := Complex.zero_re, map_add' := Complex.add_re }

source

@[simp]

theorem Complex.coe_reAddGroupHom :

⇑Complex.reAddGroupHom = Complex.re

source

def Complex.imAddGroupHom :

ℂ →+ ℝ

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

Equations

Complex.imAddGroupHom = { toFun := Complex.im, map_zero' := Complex.zero_im, map_add' := Complex.add_im }

source

@[simp]

theorem Complex.coe_imAddGroupHom :

⇑Complex.imAddGroupHom = Complex.im

Cast lemmas #

source

noncomputable instance Complex.instNNRatCast :

NNRatCast ℂ

Equations

Complex.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => ↑↑q }

source

noncomputable instance Complex.instRatCast :

RatCast ℂ

Equations

Complex.instRatCast = { ratCast := fun (q : ℚ) => ↑↑q }

source

@[simp]

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

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

source

@[simp]

theorem Complex.ofReal_natCast (n : ℕ) :

↑↑n = ↑n

source

@[simp]

theorem Complex.ofReal_intCast (n : ℤ) :

↑↑n = ↑n

source

@[simp]

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

↑↑q = ↑q

source

@[simp]

theorem Complex.ofReal_ratCast (q : ℚ) :

↑↑q = ↑q

source

@[deprecated Complex.ofReal_ratCast]

theorem Complex.ofReal_rat_cast (q : ℚ) :

↑↑q = ↑q

Alias of Complex.ofReal_ratCast.

source

@[simp]

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

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

source

@[simp]

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

(OfNat.ofNat n).im = 0

source

@[simp]

theorem Complex.natCast_re (n : ℕ) :

(↑n).re = ↑n

source

@[simp]

theorem Complex.natCast_im (n : ℕ) :

(↑n).im = 0

source

@[simp]

theorem Complex.intCast_re (n : ℤ) :

(↑n).re = ↑n

source

@[simp]

theorem Complex.intCast_im (n : ℤ) :

(↑n).im = 0

source

@[simp]

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

(↑q).re = ↑q

source

@[simp]

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

(↑q).im = 0

source

@[simp]

theorem Complex.ratCast_re (q : ℚ) :

(↑q).re = ↑q

source

@[simp]

theorem Complex.ratCast_im (q : ℚ) :

(↑q).im = 0

source

@[deprecated Complex.ratCast_im]

theorem Complex.rat_cast_im (q : ℚ) :

(↑q).im = 0

Alias of Complex.ratCast_im.

source

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

↑(n • r) = n • ↑r

source

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

↑(n • r) = n • ↑r

Complex conjugation #

source

instance Complex.instStarRing :

StarRing ℂ

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.

Equations