English
There is a canonical map from the root set of p in p.SplittingField to the root set of p in E, defined using the algebra map and the tower structure.
Русский
Существует каноническое отображение между множеством корней p в p.SplittingField и множеством корней p в E, определяемое через алгебраическую карту и торовую структуру.
LaTeX
$$$\\mathrm{mapRoots}_{p,E}: (p.{\\rootSet})\\,p.SplittingField \\to (p.{\\rootSet})\\,E$$$
Lean4
/-- The function taking `rootSet p p.SplittingField` to `rootSet p E`. This is actually a bijection,
see `Polynomial.Gal.mapRoots_bijective`. -/
def mapRoots [Fact (p.Splits (algebraMap F E))] : rootSet p p.SplittingField → rootSet p E :=
Set.MapsTo.restrict (IsScalarTower.toAlgHom F p.SplittingField E) _ _ <| rootSet_mapsTo _
