galActionHom — Mathlib

English

There is a natural embedding of p.Gal into the group of permutations of the roots of p in E, given by the action homomorphism.

Русский

Существует естественное вложение p.Gal в группу перестановок корней p в E, задаваемое действием галой-группы.

LaTeX

$$$\\mathrm{galActionHom} : p.Gal \\to^* \\mathrm{Equiv.Perm}(p.rootSet E) $$$

Lean4

/-- `Polynomial.Gal.galAction` as a permutation representation -/
def galActionHom [Fact (p.Splits (algebraMap F E))] : p.Gal →* Equiv.Perm (rootSet p E) :=
  MulAction.toPermHom _ _

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