roots_X_pow_char_sub_C_pow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem roots_X_pow_char_sub_C_pow {y : R} {m : ℕ} :
    ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y} :=
  by
  have H := roots_X_pow_char_pow_sub_C_pow (p := p) (n := 1) (y := y) (m := m)
  rwa [pow_one, iterateFrobeniusEquiv_one] at H

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