English
Over a perfect ring of characteristic p, the roots of expand R(p^n) f are exactly p^n copies of the roots of f transported by the inverse Frobenius equivalence.
Русский
В идеальном кольце характеристикой p корни expand_R(p^n) f состоят ровно из p^n копий корней f, перенесённых через обратное равенство Фробениуса.
LaTeX
$$$\operatorname{roots}(\operatorname{expand}_R(p^n, f)) = p^n \;\cdot\; \operatorname{map}((\operatorname{iterateFrobeniusEquiv} R\, p\, n).\mathrm{symm}, \operatorname{roots}(f))$$$
Lean4
theorem roots_expand_pow : (expand R (p ^ n) f).roots = p ^ n • f.roots.map (iterateFrobeniusEquiv R p n).symm := by
classical
refine ext' fun r ↦ ?_
rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map, count_eq_card_filter_eq]; congr;
ext
exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm
