instGroupAbsoluteGaloisGroup — Mathlib

English

There is a natural group structure on the absolute Galois group given by field automorphisms of the algebraic closure fixing the base field.

Русский

Существует естественная структура группы на абсолютной Галуа-группе, данная автоморфизмами поля алгебраического замыкания, фиксирующими базовое поле.

LaTeX

$$$$\text{instGroupAbsoluteGaloisGroup: }\text{Group}(\mathrm{Field.absoluteGaloisGroup}\,K)$$$$

Lean4

noncomputable instance : Group (G_K K) :=
  AlgEquiv.aut

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