absoluteGaloisGroup — Mathlib

English

The absolute Galois group of K is the Galois group of the algebraic closure of K over K.

Русский

Полная Галуа-группа K — это Галуа-группа над алгебраическим замыканием K над K.

LaTeX

$$$$\text{AbsoluteGaloisGroup}(K) = \mathrm{Gal}(\overline{K}/K)$$$$

Lean4

/-- The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
  where `K^al` is an algebraic closure of `K`. -/
def absoluteGaloisGroup :=
  AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K

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