roots_expand_pow_map_iterateFrobenius

English

The roots of expand_R(p^n) f, when mapped by iterateFrobenius, correspond to p^n times the roots of f.

Русский

Корни expand_R(p^n) f, отображённые iterateFrobenius, соответствуют p^n удвоенному корням f.

LaTeX

$$$\left(\operatorname{roots}(\operatorname{expand}_R(p^n, f))\right)^{\text{map}}(\operatorname{iterateFrobenius} R\, p\, n) = p^n \cdot \operatorname{roots}(f)$$$

Lean4

theorem roots_expand_pow_map_iterateFrobenius :
    (expand R (p ^ n) f).roots.map (iterateFrobenius R p n) = p ^ n • f.roots := by
  simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul, Multiset.map_map, comp_apply,
    RingEquiv.apply_symm_apply, map_id']

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