profiniteGalGrp — Mathlib

English

Gal(K/k) is viewed as a profinite group via the profinite group of automorphisms of K over k.

Русский

Gal(K/k) рассматривается как профинитная группа через группу автоморфизмов K над k.

LaTeX

$$$\text{profiniteGalGrp } k K = \mathrm{ProfiniteGrp}.of(K \simeq_k K)$$$

Lean4

/-- `Gal(K/k)` as a profinite group as there is
a `ContinuousMulEquiv` to a `ProfiniteGrp` given above -/
noncomputable def profiniteGalGrp [IsGalois k K] : ProfiniteGrp :=
  ProfiniteGrp.of (K ≃ₐ[k] K)

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