rootsExpandPowEquivRoots_apply — Mathlib

English

Applying iterateFrobenius to the roots of expand_R(p^n) f yields f.roots as Finset.

Русский

Применение iterateFrobenius к корням expand_R(p^n) f дает корни f как Finset.

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

@[simp]
theorem rootsExpandPowEquivRoots_apply (n : ℕ) (x) : (rootsExpandPowEquivRoots p f n x : R) = x ^ p ^ n :=
  rfl

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