roots_X_pow_char_pow_sub_C_pow — Mathlib

English

The roots of ((X^{p^n} − C y)^m) are (m p^n) copies of the inverse Frobenius image of y.

Русский

Корни из ((X^{p^n} − C y)^m) состоят из (m p^n) копий обратного образа y по Фробениусу.

LaTeX

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

Lean4

theorem roots_X_pow_char_pow_sub_C_pow {y : R} {m : ℕ} :
    ((X ^ p ^ n - C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y} := by
  rw [roots_pow, roots_X_pow_char_pow_sub_C, mul_smul]

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