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 #
Complex numbers consist of two Real
s: a real part re
and an imaginary part im
.
Equations
- termℂ = Lean.ParserDescr.node `termℂ 1024 (Lean.ParserDescr.symbol "ℂ")
Instances For
Equations
The natural inclusion of the real numbers into the complex numbers.
Equations
- ↑r = { re := r, im := 0 }
Instances For
Alias of Complex.ofReal
.
The natural inclusion of the real numbers into the complex numbers.
Equations
Instances For
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
Instances For
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))
Instances For
Equations
- Complex.instAdd = { add := fun (z w : ℂ) => { re := z.re + w.re, im := z.im + w.im } }
Equations
- Complex.instNeg = { neg := fun (z : ℂ) => { re := -z.re, im := -z.im } }
Equations
- Complex.instSub = { sub := fun (z w : ℂ) => { re := z.re - w.re, im := z.im - w.im } }
The natural AddEquiv
from ℂ
to ℝ × ℝ
.
Equations
- Complex.equivRealProdAddHom = { toEquiv := Complex.equivRealProd, map_add' := Complex.equivRealProdAddHom.proof_1 }
Instances For
Commutative ring instance and lemmas #
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
Instances For
Equations
- One or more equations did not get rendered due to their size.
This shortcut instance ensures we do not find Ring
via the noncomputable Complex.field
instance.
Equations
- Complex.instRing = inferInstance
This shortcut instance ensures we do not find CommSemiring
via the noncomputable
Complex.field
instance.
Equations
- Complex.instCommSemiring = inferInstance
This shortcut instance ensures we do not find Semiring
via the noncomputable
Complex.field
instance.
Equations
- Complex.instSemiring = inferInstance
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 }
Instances For
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 }
Instances For
Cast lemmas #
Equations
- Complex.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => ↑↑q }
Equations
- Complex.instRatCast = { ratCast := fun (q : ℚ) => ↑↑q }
Alias of Complex.ofReal_ratCast
.
Alias of Complex.ratCast_im
.
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
.
Alias of Complex.conj_natCast
.
Norm squared #
The norm squared function.
Equations
- Complex.normSq = { toFun := fun (z : ℂ) => z.re * z.re + z.im * z.im, map_zero' := Complex.normSq.proof_1, map_one' := Complex.normSq.proof_2, map_mul' := Complex.normSq.proof_3 }
Instances For
Alias of Complex.normSq_natCast
.
Alias of Complex.normSq_intCast
.
Alias of Complex.normSq_ratCast
.
The coercion ℝ → ℂ
as a RingHom
.
Equations
- Complex.ofRealHom = { toFun := fun (x : ℝ) => ↑x, map_one' := Complex.ofReal_one, map_mul' := Complex.ofReal_mul, map_zero' := Complex.ofReal_zero, map_add' := Complex.ofReal_add }
Instances For
Inversion #
Equations
- Complex.instInv = { inv := fun (z : ℂ) => (starRingEnd ℂ) z * ↑(Complex.normSq z)⁻¹ }
Field instance and lemmas #
Equations
- One or more equations did not get rendered due to their size.
Alias of Complex.div_natCast
.
Alias of Complex.div_intCast
.
Alias of Complex.div_ratCast
.
Alias of Complex.div_ratCast_im
.
Characteristic zero #
A complex number z
plus its conjugate conj z
is 2
times its real part.
A complex number z
minus its conjugate conj z
is 2i
times its imaginary part.
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.
Equations
- One or more equations did not get rendered due to their size.
The preimage under equivRealProd
of s ×ˢ t
is s ×ℂ t
.