roots_expand — Mathlib

English

For a polynomial f over a domain of characteristic p, the roots of expand R p f are p times the roots of f transported by Frobenius inverse.

Русский

Для многочлена f над областью с характеристикой p корни expand_R(p, f) равны p-копиям корней f, перенесённых через обратное отображение Фробениуса.

LaTeX

$$$\operatorname{roots}(\operatorname{expand}_R(p, f)) = p \;\cdot\; \operatorname{map}(\operatorname{frobeniusEquiv} R\, p, \operatorname{roots}(f))^{\mathrm{symm}}$$$

Lean4

theorem roots_expand : (expand R p f).roots = p • f.roots.map (frobeniusEquiv R p).symm :=
  by
  conv_lhs => rw [← pow_one p, roots_expand_pow, iterateFrobeniusEquiv_eq_pow, pow_one]
  rfl

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