fixingSubgroup_isClosed — Mathlib

English

Let E/K be finite; the subgroup Gal(L/E) is closed in Aut_K(L).

Русский

Пусть E/K конечно; Gal(L/E) замкнута в Aut_K(L).

LaTeX

$$$IsClosed\\ (E.fixingSubgroup : Set (L \\simeq_K L))$$$

Lean4

/-- Given a tower of fields `L/E/K`, with `E/K` finite, the subgroup `Gal(L/E) ≤ L ≃ₐ[K] L` is
  closed. -/
theorem fixingSubgroup_isClosed {K L : Type*} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L)
    [FiniteDimensional K E] : IsClosed (E.fixingSubgroup : Set (L ≃ₐ[K] L)) :=
  OpenSubgroup.isClosed ⟨E.fixingSubgroup, E.fixingSubgroup_isOpen⟩

Похожие утверждения