roots_expand_image_frobenius — Mathlib

English

There is a natural bijection between the roots of expand R(p^n) f and the roots of f, given by the Frobenius-related map.

Русский

Существует естественная биекция между корнями expand_R(p^n) f и корнями f, задаваемая отображением, связанным с Фробениусом.

LaTeX

$$$\operatorname{rootsExpandPowEquivRoots} (p, f, n) : (\expand_R(p^n, f).\text{roots}) \cong (\operatorname{roots}(f))$$$

Lean4

theorem roots_expand_image_frobenius [DecidableEq R] :
    (expand R p f).roots.toFinset.image (frobenius R p) = f.roots.toFinset := by
  rw [Finset.image_toFinset, roots_expand_map_frobenius, (roots f).toFinset_nsmul _ (expChar_pos R p).ne']

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