proj — Mathlib

English

The finite Galois group Gal(L/k) is a finite group.

Русский

Конечная Галуа-группа Gal(L/k) является конечной группой.

LaTeX

$$finGaloisGroup(L) : FiniteGrp$$

Lean4

/-- The projection map from `lim Gal(L/k)` to a specific `Gal(L/k)`. -/
noncomputable def proj (L : FiniteGaloisIntermediateField k K) :
    limit (asProfiniteGaloisGroupFunctor k K) →* (L ≃ₐ[k] L)
    where
  toFun g := g.val (op L)
  map_one' := rfl
  map_mul' _ _ := rfl

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