roots_X_pow_char_sub_C — Mathlib

English

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

Русский

Для y ∈ R корни X^p − C y равны p копиям обратного образа y по Фробениусу.

LaTeX

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

Lean4

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

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