Embeddings of number fields #
This file defines the embeddings of a number field and, in particular, the embeddings into the field of complex numbers.
Main Definitions and Results #
NumberField.Embeddings.range_eval_eq_rootSet_minpoly
: letx ∈ K
withK
a number field and letA
be an algebraically closed field of char. 0. Then the images ofx
under the embeddings ofK
inA
are exactly the roots inA
of the minimal polynomial ofx
overℚ
.NumberField.Embeddings.pow_eq_one_of_norm_eq_one
: an algebraic integer whose conjugates are all of norm one is a root of unity.
Tags #
number field, embeddings
There are finitely many embeddings of a number field.
Equations
The number of embeddings of a number field is equal to its finrank.
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 ℚ
.
Let 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.
An embedding into a normed division ring defines a place of K
Equations
Instances For
A (random) lift of the complex embedding φ : k →+* ℂ
to an extension K
of k
.
Equations
Instances For
An embedding into ℂ
is real if it is fixed by complex conjugation.