Embeddings of number fields #
This file defines the embeddings of a number field into an algebraic closed field.
Main Definitions and Results #
x ∈ Kwith
Knumber field and let
Abe an algebraic closed field of char. 0, then the images of
xby the embeddings of
Aare exactly the roots in
Aof the minimal polynomial of
NumberField.Embeddings.pow_eq_one_of_norm_eq_one: an algebraic integer whose conjugates are all of norm one is a root of unity.
NumberField.InfinitePlace: the type of infinite places of a number field
NumberField.InfinitePlace.mk_eq_iff: two complex embeddings define the same infinite place iff they are equal or complex conjugates.
NumberField.InfinitePlace.prod_eq_abs_norm: the infinite part of the product formula, that is for
x ∈ K, we have
Π_w ‖x‖_w = |norm(x)|where the product is over the infinite place
‖·‖_wis the normalized absolute value for
number field, embeddings, places, infinite places
There are finitely many embeddings of a number field.
A be an algebraically closed field and let
x ∈ K, with
K a number field.
The images of
x by the embeddings of
A are exactly the roots in
the minimal polynomial of
B be a real number. The set of algebraic integers in
K whose conjugates are all
smaller in norm than
B is finite.
An algebraic integer whose conjugates are all of norm one is a root of unity.
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