Gal — Mathlib

English

For a polynomial p over F, the Galois group Gal(p) is defined as the automorphism group of its splitting field p.SplittingField over F.

Русский

Для многочлена p над полем F группа Галуа Gal(p) определяется как группа автоморфизмов разложения p над полем F на поле разложения p.SplittingField.

LaTeX

$$$\mathrm{Gal}:= p.SplittingField \cong_F p.SplittingField$$$

Lean4

/-- The Galois group of a polynomial. -/
def Gal :=
  p.SplittingField ≃ₐ[F] p.SplittingField
deriving Group, Fintype, EquivLike, AlgEquivClass

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