English
Let R be a commutative semiring, p a prime with characteristic p. For any f in the p-th perfection of R and any natural number n, the p-th power Frobenius shifts the coefficient: coeff R p (n+1) (f^p) = coeff R p n f.
Русский
Пусть R — коммутативное полуполе, p — простое число с характеристикой p. Для любого f в перфекции порядка p над R и любого n ∈ ℕ, коэффициент после возведения в p-ую степень сдвигается: coeff_R_p(n+1, f^p) = coeff_R_p(n, f).
LaTeX
$$$\\operatorname{coeff} R p (n+1) (f^p) = \\operatorname{coeff} R p n f$$$
Lean4
theorem coeff_pow_p (f : Ring.Perfection R p) (n : ℕ) : coeff R p (n + 1) (f ^ p) = coeff R p n f := by
rw [RingHom.map_pow]; exact f.2 n
