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
.
Instances For
- CStarAlgebra.instNonnegSpectrumClassComplexNonUnital
- CStarAlgebra.instNonnegSpectrumClassComplexUnital
- Circle.instCoeOut
- Complex.UnitDisc.instCoe
- Complex.addCommGroup
- Complex.addGroupWithOne
- Complex.borelSpace
- Complex.canLift
- Complex.commRing
- Complex.distribSMul
- Complex.hasMeasurablePow
- Complex.instAdd
- Complex.instAlgebraOfReal
- Complex.instCharZero
- Complex.instCoeReal
- Complex.instCommSemiring
- Complex.instCompleteSpace
- Complex.instContinuousStar
- Complex.instDenselyNormedField
- Complex.instDistribMulActionOfReal
- Complex.instDivInvMonoid
- Complex.instField
- Complex.instFiniteDimensionalReal
- Complex.instInhabited
- Complex.instInv
- Complex.instIsCentralScalarOfReal
- Complex.instIsComplete
- Complex.instIsScalarTowerOfReal
- Complex.instModule
- Complex.instMul
- Complex.instNNRatCast
- Complex.instNeg
- Complex.instNontrivial
- Complex.instNorm
- Complex.instNormedAddCommGroup
- Complex.instNormedAlgebraOfReal
- Complex.instNormedField
- Complex.instOne
- Complex.instPow
- Complex.instProperSpace
- Complex.instRCLike
- Complex.instRatCast
- Complex.instRepr
- Complex.instRing
- Complex.instSMulCommClassOfReal
- Complex.instSemiring
- Complex.instStarModuleReal
- Complex.instStarRing
- Complex.instSub
- Complex.instT2Space
- Complex.instTietzeExtension
- Complex.instZero
- Complex.isAlgClosed
- Complex.measurableSpace
- Complex.mulAction
- CuspForm.funLike
- CuspForm.instModuleComplex
- GaussianInt.instCoeComplex
- IsStarNormal.instContinuousFunctionalCalculus
- IsStarNormal.instNonUnitalContinuousFunctionalCalculus
- ModularForm.SLAction
- ModularForm.funLike
- ModularForm.instGAlgebra
- ModularForm.instModuleComplex
- ModularForm.instSlashActionIntSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroupGLPosForallUpperHalfPlaneComplex
- ModularForm.subgroupAction
- Quaternion.instCoeComplexReal
- SlashInvariantForm.funLike
- SlashInvariantForm.instModuleComplex
- UpperHalfPlane.canLift
- UpperHalfPlane.instChartedSpaceComplex
- UpperHalfPlane.instCoeOutComplex
- WeakDual.CharacterSpace.instStarHomClass
- WeakDual.Complex.instStarHomClass
- WithCStarModule.instCStarModuleComplex
- WithCStarModule.instNormedSpaceComplexForall
- WithCStarModule.instNormedSpaceComplexProd
- instInnerProductSpaceRealComplex
- instInnerProductSpaceRealComplex_1
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 "ℂ")
Equations
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
Equations
- Complex.instCoeReal = { coe := Complex.ofReal' }
Equations
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
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))
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 }
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
- 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 }
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 }
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 }
Alias of Complex.normSq_natCast
.
Alias of Complex.normSq_intCast
.
Alias of Complex.normSq_ratCast
.
The coercion ℝ → ℂ
as a RingHom
.
Equations
- Complex.ofReal = { toFun := fun (x : ℝ) => ↑x, map_one' := Complex.ofReal_one, map_mul' := Complex.ofReal_mul, map_zero' := Complex.ofReal_zero, map_add' := Complex.ofReal_add }
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.