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.

@[protected, instance]
noncomputable def complex.has_norm  :
Equations
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]

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

Equations
theorem complex.dist_eq (z w : ) :
theorem complex.dist_eq_re_im (z w : ) :
has_dist.dist z w = real.sqrt ((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)
@[simp]
theorem complex.dist_mk (x₁ y₁ x₂ y₂ : ) :
has_dist.dist {re := x₁, im := y₁} {re := x₂, im := y₂} = real.sqrt ((x₁ - x₂) ^ 2 + (y₁ - y₂) ^ 2)
theorem complex.dist_of_re_eq {z w : } (h : z.re = w.re) :
theorem complex.edist_of_re_eq {z w : } (h : z.re = w.re) :
theorem complex.dist_of_im_eq {z w : } (h : z.im = w.im) :
theorem complex.edist_of_im_eq {z w : } (h : z.im = w.im) :
@[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) :
@[simp, norm_cast]
@[simp, norm_cast]
theorem complex.nnnorm_nat (n : ) :
@[simp, norm_cast]
theorem complex.nnnorm_eq_one_of_pow_eq_one {ζ : } {n : } (h : ζ ^ n = 1) (hn : n 0) :
theorem complex.norm_eq_one_of_pow_eq_one {ζ : } {n : } (h : ζ ^ n = 1) (hn : n 0) :
ζ = 1
noncomputable def complex.re_clm  :

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

Equations
@[simp]
noncomputable def complex.im_clm  :

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

The determinant of conj_lie, as a linear map.

@[simp]

The determinant of conj_lie, as a linear equiv.

The only continuous ring homomorphisms from to are the identity and the complex conjugation.

noncomputable def complex.conj_cle  :

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

Equations

Linear isometry version of the canonical embedding of in .

Equations
@[continuity]

The only continuous ring homomorphism from to is the identity.

noncomputable def complex.of_real_clm  :

Continuous linear map version of the canonical embedding of in .

Equations
@[protected, instance]
noncomputable def complex.is_R_or_C  :
Equations
theorem complex.eq_coe_norm_of_nonneg {z : } (hz : 0 z) :

The natural add_equiv from to ℝ × ℝ.

Equations

The natural linear_equiv from to ℝ × ℝ.

Equations
@[simp]
theorem complex.has_sum_iff {α : Type u_1} (f : α ) (c : ) :
has_sum f c has_sum (λ (x : α), (f x).re) c.re has_sum (λ (x : α), (f x).im) c.im
@[simp]
@[simp]