English
Let f be a polynomial over a domain R. Then the roots of expand R p f, after applying Frobenius map, correspond to p times the roots of f via a map on multisets; i.e., map (frobenius R p) (expand R p f).roots = p · f.roots.
Русский
Пусть f — многочлен над области R. Корни expand(R,p,f), применяя Frobenius, соответствуют корням f с кратностью p; отображение через мультисеты: map (frobenius R p) (expand R p f).roots = p · f.roots.
LaTeX
$$$\operatorname{map}(\text{frobenius } R p) (\operatorname{roots}(\expan d R p\, f)) = p \cdot \operatorname{roots}(f)$$$
Lean4
theorem roots_expand_map_frobenius_le : (expand R p f).roots.map (frobenius R p) ≤ p • f.roots :=
by
rw [← iterateFrobenius_one]
convert ← roots_expand_pow_map_iterateFrobenius_le p 1 f <;> apply pow_one
