mathlibdocumentation

analysis.complex.basic

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.

@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
def complex.normed_algebra {R : Type u_1} [normed_field R] [ ] :
Equations
@[simp]
theorem complex.norm_eq_abs (z : ) :
theorem complex.dist_eq (z w : ) :
dist z w = complex.abs (z - w)
@[simp]
theorem complex.norm_real (r : ) :
@[simp]
theorem complex.norm_rat (r : ) :
@[simp]
theorem complex.norm_nat (n : ) :
@[simp]
theorem complex.norm_int {n : } :
theorem complex.norm_int_of_nonneg {n : } (hn : 0 n) :
def complex.re_clm  :

Continuous linear map version of the real part function, from ℂ to ℝ.

Equations
@[simp]
@[simp]
theorem complex.re_clm_apply (z : ) :
@[simp]
theorem complex.re_clm_norm  :
def complex.im_clm  :

Continuous linear map version of the real part function, from ℂ to ℝ.

Equations
@[simp]
@[simp]
theorem complex.im_clm_apply (z : ) :
@[simp]
theorem complex.im_clm_norm  :
def complex.conj_li  :

The complex-conjugation function from ℂ to itself is an isometric linear map.

Equations

Continuous linear map version of the conj function, from ℂ to ℂ.

Equations
@[simp]
@[simp]
theorem complex.conj_clm_apply (z : ) :
@[simp]
theorem complex.conj_clm_norm  :

Linear isometry version of the canonical embedding of ℝ in ℂ.

Equations

Continuous linear map version of the canonical embedding of ℝ in ℂ.

Equations
@[simp]
@[simp]
theorem complex.of_real_clm_apply (x : ) :
@[simp]
@[instance]
Equations
@[simp]
theorem is_R_or_C.re_to_complex {x : } :
= x.re
@[simp]
theorem is_R_or_C.im_to_complex {x : } :
= x.im
@[simp]
theorem is_R_or_C.conj_to_complex {x : } :
@[simp]
@[simp]
@[simp]
theorem is_R_or_C.abs_to_complex {x : } :