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]