Splitting fields over number fields are number fields #
The splitting field f.SplittingField of a polynomial f over a number field K is a finite
extension of K, hence a number field. In particular the splitting field of a rational
polynomial is a number field, so its Galois group f.Gal is the Galois group of a number field
and the arithmetic of 𝓞 f.SplittingField (primes, Frobenius elements) is available in it
directly.
Main results #
Polynomial.SplittingField.instNumberField: the splitting field of a polynomial over a number field is a number field.
instance
Polynomial.SplittingField.instNumberField
{K : Type u_1}
[Field K]
[NumberField K]
(f : Polynomial K)
:
The splitting field of a polynomial over a number field is a number field.