English
Let R be a domain with characteristic p and f a polynomial over R. Then the p^n-th Frobenius image of the roots of expand R(p^n) f lies inside the roots set of f.
Русский
Пусть R — область с характеристикой p и f — многочлен над R. Тогда образ под действием p^n-й операции Фробениуса от корней expand_R(p^n) f лежит в множестве корней f.
LaTeX
$$$\operatorname{image}_{\mathrm{Finset}}\bigl(\iterateFrobenius R\,p\,n,\; (\operatorname{roots}(\operatorname{expand}_R(p^n, f)))^{\text{toFinset}}\bigr) \subseteq (\operatorname{roots}(f))^{\text{toFinset}}$$$
Lean4
theorem roots_expand_pow_image_iterateFrobenius_subset [DecidableEq R] :
(expand R (p ^ n) f).roots.toFinset.image (iterateFrobenius R p n) ⊆ f.roots.toFinset :=
by
rw [Finset.image_toFinset, ← (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne', toFinset_subset]
exact subset_of_le (roots_expand_pow_map_iterateFrobenius_le p n f)
