mathlib3 documentation


Embeddings of number fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines the embeddings of a number field into an algebraic closed field.

Main Results #

Tags #

number field, embeddings, places, infinite places

@[protected, instance]
noncomputable def number_field.embeddings.ring_hom.fintype (K : Type u_1) [field K] [number_field K] (A : Type u_2) [field A] [char_zero A] :

There are finitely many embeddings of a number field.


The number of embeddings of a number field is equal to its finrank.

@[protected, instance]
theorem number_field.embeddings.range_eval_eq_root_set_minpoly (K : Type u_1) (A : Type u_2) [field K] [number_field K] [field A] [algebra A] [is_alg_closed A] (x : K) :
set.range (λ (φ : K →+* A), φ x) = (minpoly x).root_set A

Let A be an algebraically closed field and let x ∈ K, with K a number field. The images of x by the embeddings of K in A are exactly the roots in A of the minimal polynomial of x over .

theorem number_field.embeddings.finite_of_norm_le (K : Type u_1) [field K] [number_field K] (A : Type u_2) [normed_field A] [is_alg_closed A] [normed_algebra A] (B : ) :
{x : K | is_integral x (φ : K →+* A), φ x B}.finite

Let B be a real number. The set of algebraic integers in K whose conjugates are all smaller in norm than B is finite.

theorem number_field.embeddings.pow_eq_one_of_norm_eq_one (K : Type u_1) [field K] [number_field K] (A : Type u_2) [normed_field A] [is_alg_closed A] [normed_algebra A] {x : K} (hxi : is_integral x) (hx : (φ : K →+* A), φ x = 1) :
(n : ) (hn : 0 < n), x ^ n = 1

An algebraic integer whose conjugates are all of norm one is a root of unity.

def {K : Type u_1} [field K] {A : Type u_2} [normed_division_ring A] [nontrivial A] (φ : K →+* A) :

An embedding into a normed division ring defines a place of K

theorem number_field.place_apply {K : Type u_1} [field K] {A : Type u_2} [normed_division_ring A] [nontrivial A] (φ : K →+* A) (x : K) :

The conjugate of a complex embedding as a complex embedding.

def number_field.complex_embedding.is_real {K : Type u_1} [field K] (φ : K →+* ) :

A embedding into is real if it is fixed by complex conjugation.


A real embedding as a ring homomorphism from K to .

noncomputable def {K : Type u_1} [field K] (φ : K →+* ) :

Return the infinite place defined by a complex embedding φ.


For an infinite place w, return an embedding φ such that w = infinite_place φ .

theorem number_field.infinite_place.eq_iff_eq {K : Type u_1} [field K] (x : K) (r : ) :
( (w : number_field.infinite_place K), w x = r) (φ : K →+* ), φ x = r
theorem number_field.infinite_place.le_iff_le {K : Type u_1} [field K] (x : K) (r : ) :
theorem number_field.infinite_place.pos_iff {K : Type u_1} [field K] {w : number_field.infinite_place K} {x : K} :
0 < w x x 0

An infinite place is real if it is defined by a real embedding.


An infinite place is complex if it is defined by a complex (ie. not real) embedding.


For w a real infinite place, return the corresponding embedding as a morphism K →+* ℝ.

noncomputable def number_field.infinite_place.mk_real (K : Type u_1) [field K] :

The map from real embeddings to real infinite places as an equiv


The map from nonreal embeddings to complex infinite places


The infinite part of the product formula : for x ∈ K, we have Π_w ‖x‖_w = |norm(x)| where ‖·‖_w is the normalized absolute value for w.