isGalois — Mathlib

English

If a finite group G acts as the Galois group of a field extension L/K (i.e., G is a finite Galois group for L/K), then the extension L/K is a Galois extension.

Русский

Если конечная группа G является Галуа-группой для расширения полей L/K, тогда расширение L/K Галуа.

LaTeX

$$$\\#G < \\infty \\quad\\land\\quad IsGaloisGroup(G,K,L) \\Rightarrow IsGalois(K,L)$$$

Lean4

/-- If `G` is a finite Galois group for `L/K`, then `L/K` is a Galois extension. -/
theorem isGalois [Finite G] [IsGaloisGroup G K L] : IsGalois K L :=
  by
  rw [← isGalois_iff_isGalois_bot, ← fixedPoints_eq_bot G]
  exact IsGalois.of_fixed_field L G

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