of_isGalois — Mathlib

English

If L/K is a finite Galois extension, then the automorphism group Aut_K(L) acts as a Galois group for L/K.

Русский

Если L/K — конечное Галуа-расширение, то группа автоморфизмов Aut_K(L) служит Галуа-группой для L/K.

LaTeX

$$IsGaloisGroup( L \\simeq_K L ) K L$$

Lean4

/-- If `L/K` is a finite Galois extension, then `L ≃ₐ[K] L` is a Galois group for `L/K`. -/
instance of_isGalois [FiniteDimensional K L] [IsGalois K L] : IsGaloisGroup (L ≃ₐ[K] L) K L
    where
  faithful := inferInstance
  commutes := inferInstance
  isInvariant := ⟨fun x ↦ (IsGalois.mem_bot_iff_fixed x).mpr⟩

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