Intermediate fields of a cyclic Galois extension #
In a finite Galois extension L/F with cyclic Galois group, an intermediate field is determined
by its degree over F: a cyclic group has at most one subgroup of each index, and the Galois
correspondence identifies [E : F] with the index of the fixing subgroup of E.
Main results #
IntermediateField.eq_of_finrank_eq_of_isCyclic: intermediate fields of a finite cyclic Galois extension with the same degree are equal.
theorem
IntermediateField.eq_of_finrank_eq_of_isCyclic
{F : Type u_1}
{L : Type u_2}
[Field F]
[Field L]
[Algebra F L]
[FiniteDimensional F L]
[IsGalois F L]
[IsCyclic Gal(L/F)]
{E₁ E₂ : IntermediateField F L}
(h : Module.finrank F ↥E₁ = Module.finrank F ↥E₂)
:
In a finite Galois extension with cyclic Galois group, two intermediate fields of the same degree are equal.