Finite Galois subextensions of a number field are number fields #
A finite Galois subextension E of an extension L / K of a number field K is a finite
extension of K, hence a number field. This is what lets the arithmetic of number fields (rings of
integers, adeles, ideles) be applied levelwise to the finite Galois subextensions of an infinite
extension such as a separable closure of K.
Main results #
FiniteGaloisIntermediateField.instNumberField: a finite Galois subextension of an extension of a number field is a number field.
instance
FiniteGaloisIntermediateField.instNumberField
{K : Type u_1}
{L : Type u_2}
[Field K]
[NumberField K]
[Field L]
[Algebra K L]
(E : FiniteGaloisIntermediateField K L)
:
A finite Galois subextension of an extension of a number field is a number field.