roots_X_pow_char_pow_sub_C — Mathlib

English

For any y in R, the roots of X^{p^n} − C y are p^n copies of the inverse Frobenius image of y.

Русский

Для любого y ∈ R корни X^{p^n} − C y состоят из p^n копий обратного образа y по Фробениусу.

LaTeX

$$$\bigl( X^{p^n} - C y \bigr).\text{roots} = p^n \cdot \{ (\operatorname{iterateFrobeniusEquiv} R\, p\, n).symm y \}$$$

Lean4

theorem roots_X_pow_char_pow_sub_C {y : R} : (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y} :=
  by
  have H := roots_expand_pow (p := p) (n := n) (f := X - C y)
  rwa [roots_X_sub_C, Multiset.map_singleton, map_sub, expand_X, expand_C] at H

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