English
For a field extension L/K, fixedByFinite K L is the set of subgroups Gal(L/E) for finite E/K.
Русский
Для расширения L/K множество fixedByFinite K L состоит из гал-галловских подгрупп Gal(L/E) для конечных E/K.
LaTeX
$$$fixedByFinite\\ (K,L) = \\{ G: Subgroup(L\\simeq_K L) \\mid \\exists E: IntermediateField K L, \\dim_K E < \\infty\\, \\wedge \\ G = Gal(L/E) \\}$$$
Lean4
/-- Given a field extension `L/K`, `fixedByFinite K L` is the set of
subsets `Gal(L/E)` of `L ≃ₐ[K] L`, where `E/K` is finite. -/
def fixedByFinite (K L : Type*) [Field K] [Field L] [Algebra K L] : Set (Subgroup (L ≃ₐ[K] L)) :=
IntermediateField.fixingSubgroup '' finiteExts K L
