English
If H is a normal subgroup of Gal(L/K), then Gal(fixedField H / K) is isomorphic to Gal(L/K)/H.
Русский
Если H нормальная подгруппа Гал( L/K ), то Gal( fixedField(H)/K ) изоморфна Gal(L/K)/H.
LaTeX
$$$\operatorname{Gal}(\operatorname{fixedField}(H)/K) \cong (\operatorname{Gal}(L/K))/H$$$
Lean4
/-- If `H` is a normal Subgroup of `Gal(L / K)`, then `Gal(fixedField H / K)` is isomorphic to
`Gal(L / K) ⧸ H`. -/
noncomputable def normalAutEquivQuotient [FiniteDimensional K L] [IsGalois K L] (H : Subgroup (L ≃ₐ[K] L))
[Subgroup.Normal H] : (L ≃ₐ[K] L) ⧸ H ≃* ((fixedField H) ≃ₐ[K] (fixedField H)) :=
(QuotientGroup.quotientMulEquivOfEq
((fixingSubgroup_fixedField H).symm.trans (fixedField H).restrictNormalHom_ker.symm)).trans <|
QuotientGroup.quotientKerEquivOfSurjective (restrictNormalHom (fixedField H)) <| restrictNormalHom_surjective L
