galActionAux — Mathlib

English

The action of p.Gal on the root set p.SplittingField is induced by restriction of algebra automorphisms to the splitting field, giving a MulAction.

Русский

Действие группы Гал(p) на множество корней p.SplittingField индуцируется ограничением алгебраических автоморфизмов к полю разложения, образуя действие группы.

LaTeX

$$$\\text{MulAction } p.Gal\\ (p.rootSet\\, p.SplittingField).\\text{Elem}$$$

Lean4

instance galActionAux : MulAction p.Gal (rootSet p p.SplittingField)
    where
  smul ϕ := Set.MapsTo.restrict ϕ _ _ <| rootSet_mapsTo ϕ.toAlgHom
  one_smul _ := by ext; rfl
  mul_smul _ _ _ := by ext; rfl

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