galAction — Mathlib

English

The action of p.Gal on the roots of p in E is well-defined, turning p.Gal into a group of permutations of the roots.

Русский

Действие группы Гал(p) на корни p в E определено и превращает p.Gal в подгруппу перестановок корней.

LaTeX

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

Lean4

/-- The action of `gal p` on the roots of `p` in `E`. -/
instance galAction [Fact (p.Splits (algebraMap F E))] : MulAction p.Gal (rootSet p E)
    where
  one_smul _ := by simp only [smul_def, Equiv.apply_symm_apply, one_smul]
  mul_smul _ _ _ := by simp only [smul_def, Equiv.symm_apply_apply, mul_smul]

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