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 #
The natural inclusion of the real numbers into the complex numbers.
The name Complex.ofReal
is reserved for the bundled homomorphism.
Instances For
Commutative ring instance and lemmas #
This shortcut instance ensures we do not find Ring
via the noncomputable Complex.field
instance.
This shortcut instance ensures we do not find CommSemiring
via the noncomputable
Complex.field
instance.
This shortcut instance ensures we do not find Semiring
via the noncomputable
Complex.field
instance.
The "real part" map, considered as an additive group homomorphism.
Instances For
The "imaginary part" map, considered as an additive group homomorphism.
Instances For
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
.
Norm squared #
Inversion #
Cast lemmas #
Field instance and lemmas #
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.
Absolute value #
The complex absolute value function, defined as the square root of the norm squared.
Instances For
Cauchy sequences #
The real part of a complex Cauchy sequence, as a real Cauchy sequence.
Instances For
The imaginary part of a complex Cauchy sequence, as a real Cauchy sequence.
Instances For
The limit of a Cauchy sequence of complex numbers.
Instances For
The complex conjugate of a complex Cauchy sequence, as a complex Cauchy sequence.
Instances For
The absolute value of a complex Cauchy sequence, as a real Cauchy sequence.