roots_expand_image_frobenius_subset

English

For any DecidableEq R, the roots of expand R p f, mapped by the Frobenius map, are contained in the roots of f.

Русский

Для любого DecidableEq R корни expand R p f, отображенные Фробениусом, вложены в корни f.

LaTeX

$$$\operatorname{image}_{\mathrm{Finset}}\bigl(\operatorname{frobenius} \; R\; p,\; (\operatorname{roots}(\operatorname{expand}_R(p, f)))^{\text{toFinset}}\bigr) \subseteq (\operatorname{roots}(f))^{\text{toFinset}}$$$

Lean4

theorem roots_expand_image_frobenius_subset [DecidableEq R] :
    (expand R p f).roots.toFinset.image (frobenius R p) ⊆ f.roots.toFinset :=
  by
  rw [← iterateFrobenius_one]
  convert ← roots_expand_pow_image_iterateFrobenius_subset p 1 f
  apply pow_one

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