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:
re_clm
im_clm
of_real_clm
conj_clm
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 of_real_li
and conj_li
.
We also register the fact that ℂ
is an is_R_or_C
field.
Equations
Equations
- complex.normed_group = normed_group.of_core ℂ complex.normed_group._proof_1
Equations
- complex.normed_field = {to_has_norm := {norm := complex.abs}, to_field := {add := field.add complex.field, add_assoc := _, zero := field.zero complex.field, zero_add := _, add_zero := _, neg := field.neg complex.field, sub := field.sub complex.field, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := field.mul complex.field, mul_assoc := _, one := field.one complex.field, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := field.inv complex.field, div := field.div complex.field, div_eq_mul_inv := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}, to_metric_space := normed_group.to_metric_space complex.normed_group, dist_eq := complex.normed_field._proof_1, norm_mul' := complex.abs_mul}
Equations
- complex.nondiscrete_normed_field = {to_normed_field := complex.normed_field, non_trivial := complex.nondiscrete_normed_field._proof_1}
Equations
Continuous linear map version of the real part function, from ℂ
to ℝ
.
Equations
- complex.re_clm = complex.re_lm.mk_continuous 1 complex.re_clm._proof_1
Continuous linear map version of the real part function, from ℂ
to ℝ
.
Equations
- complex.im_clm = complex.im_lm.mk_continuous 1 complex.im_clm._proof_1
The complex-conjugation function from ℂ
to itself is an isometric linear map.
Equations
- complex.conj_li = {to_linear_map := complex.conj_lm, norm_map' := complex.conj_li._proof_1}
Continuous linear map version of the conj function, from ℂ
to ℂ
.
Linear isometry version of the canonical embedding of ℝ
in ℂ
.
Equations
- complex.of_real_li = {to_linear_map := complex.of_real_lm, norm_map' := complex.of_real_li._proof_1}
Continuous linear map version of the canonical embedding of ℝ
in ℂ
.
Equations
- complex.is_R_or_C = {to_nondiscrete_normed_field := complex.nondiscrete_normed_field, to_normed_algebra := complex.normed_algebra (normed_algebra.id ℝ), to_complete_space := complex.is_R_or_C._proof_1, re := {to_fun := complex.re, map_zero' := complex.zero_re, map_add' := complex.add_re}, im := {to_fun := complex.im, map_zero' := complex.zero_im, map_add' := complex.add_im}, conj := complex.conj, I := complex.I, I_re_ax := complex.is_R_or_C._proof_2, I_mul_I_ax := complex.is_R_or_C._proof_3, re_add_im_ax := complex.is_R_or_C._proof_4, of_real_re_ax := complex.is_R_or_C._proof_5, of_real_im_ax := complex.is_R_or_C._proof_6, mul_re_ax := complex.is_R_or_C._proof_7, mul_im_ax := complex.is_R_or_C._proof_8, conj_re_ax := complex.is_R_or_C._proof_9, conj_im_ax := complex.is_R_or_C._proof_10, conj_I_ax := complex.is_R_or_C._proof_11, norm_sq_eq_def_ax := complex.is_R_or_C._proof_12, mul_im_I_ax := complex.is_R_or_C._proof_13, inv_def_ax := complex.is_R_or_C._proof_14, div_I_ax := complex.div_I}