English
For any y, the roots of X^{p^n} − C y are the p^n copies of (iterateFrobeniusEquiv R p n).symm y.
Русский
Для любого y корни X^{p^n} − C y равны p^n копиям (iterateFrobeniusEquiv R p n).symm y.
LaTeX
$$$\bigl( X^{p^n} - C y \bigr).\text{roots} = p^n \cdot \{ (\operatorname{iterateFrobeniusEquiv} R p n).symm y \}$$$
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 ^ n) f` to the set of roots of `f`.
It's given by `x ↦ x ^ (p ^ n)`, see `rootsExpandPowToRoots_apply`. -/
noncomputable def rootsExpandPowToRoots : (expand R (p ^ n) f).roots.toFinset ↪ f.roots.toFinset
where
toFun x := ⟨x ^ p ^ n, roots_expand_pow_image_iterateFrobenius_subset p n f (Finset.mem_image_of_mem _ x.2)⟩
inj' _ _ h := Subtype.ext (iterateFrobenius_inj R p n <| Subtype.ext_iff.1 h)
