English
The basic power-map under the equivalence sends a representative to its p^n-th power.
Русский
Базовая карта из представителя через эквивалент сохраняет признак степени p^n.
LaTeX
$$$(\text{rootsExpandPowEquivRoots } p\ f\ n\ x : R) = x^{p^n}$$$
Lean4
/-- If `f` is a polynomial over an integral domain `R` of characteristic `p`, then there is
a map from the set of roots of `Polynomial.expand R p f` to the set of roots of `f`.
It's given by `x ↦ x ^ p`, see `rootsExpandToRoots_apply`. -/
noncomputable def rootsExpandToRoots : (expand R p f).roots.toFinset ↪ f.roots.toFinset
where
toFun x := ⟨x ^ p, roots_expand_image_frobenius_subset p f (Finset.mem_image_of_mem _ x.2)⟩
inj' _ _ h := Subtype.ext (frobenius_inj R p <| Subtype.ext_iff.1 h)
