roots_expand_image_iterateFrobenius

English

Equality of Finset images: the Finset image of iterateFrobenius on the roots of expand_R(p^n) f equals the Finset of roots of f.

Русский

Равенство отображений по множествам: образ по iterateFrobenius от корней expand_R(p^n) f совпадает с корнями f.

LaTeX

$$$\operatorname{image}_{\mathrm{Finset}}(\iterateFrobenius R\, p\, n, (\operatorname{roots}(\operatorname{expand}_R(p^n, f)))^{\text{toFinset}}} = (\operatorname{roots}(f))^{\text{toFinset}}$$$

Lean4

theorem roots_expand_image_iterateFrobenius [DecidableEq R] :
    (expand R (p ^ n) f).roots.toFinset.image (iterateFrobenius R p n) = f.roots.toFinset := by
  rw [Finset.image_toFinset, roots_expand_pow_map_iterateFrobenius,
    (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne']

Похожие утверждения