English
For any polynomial f ∈ R[X], the expansion with respect to p equals the p-th power of f after applying the inverse Frobenius map to coefficients; i.e., expand R p f = (f.map (frobeniusEquiv R p).symm) ^ p.
Русский
Для любого многочлена f ∈ R[X] разложение относительно p равно p-й степени f после применения обратного Фробениуса к коэффициентам; т.е. expand R p f = (f.map (frobeniusEquiv R p).symm) ^ p.
LaTeX
$$$ \text{expand } R\ p\ f = \left( f.map\left( \text{frobeniusEquiv } R\ p\right)^{-1} \right)^p. $$$
Lean4
theorem polynomial_expand_eq (f : R[X]) : expand R p f = (f.map (frobeniusEquiv R p).symm) ^ p := by
rw [← (f.map (S := R) (frobeniusEquiv R p).symm).expand_char p, map_expand, map_map,
frobenius_comp_frobeniusEquiv_symm, map_id]
