mathlib documentation

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:

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_lie.

We also register the fact that is an is_R_or_C field.

@[instance]
Equations
@[instance]

The module structure from module.complex_to_real is a normed space.

Equations
@[simp]
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) :

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

Equations
@[simp]

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

Equations
@[simp]

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

Equations

Continuous linear equiv version of the conj function, from to .

Equations

Linear isometry version of the canonical embedding of in .

Equations

Continuous linear map version of the canonical embedding of in .

Equations
@[instance]
Equations
@[simp]
@[simp]