Normed space structure on ℂ
. #
This file gathers basic facts on complex numbers of an analytic nature.
Main results #
This file registers ℂ
as a normed field, expresses basic properties of the norm, and gives
tools on the real vector space structure of ℂ
. Notably, in the namespace Complex
,
it defines functions:
They are bundled versions of the real part, the imaginary part, the embedding of ℝ
in ℂ
, and
the complex conjugate as continuous ℝ
-linear maps. The last two are also bundled as linear
isometries in ofRealLi
and conjLie
.
We also register the fact that ℂ
is an IsROrC
field.
The module structure from Module.complexToReal
is a normed space.
The natural ContinuousLinearEquiv
from ℂ
to ℝ × ℝ
.
Instances For
The abs
function on ℂ
is proper.
The normSq
function on ℂ
is proper.
The only continuous ring homomorphisms from ℂ
to ℂ
are the identity and the complex
conjugation.
The only continuous ring homomorphism from ℝ
to ℂ
is the identity.
We have to repeat the lemmas about IsROrC.re
and IsROrC.im
as they are not syntactic
matches for Complex.re
and Complex.im
.
We do not have this problem with ofReal
and conj
, although we repeat them anyway for
discoverability and to avoid the need to unify 𝕜
.