English
If R has characteristic p, then the nth coefficient of Frobenius x equals x.coeff n to the p-th power.
Русский
Если характеристика R равна p, то n-й коэффициент Frobenius x равен x.coeff n в степени p.
LaTeX
$$$$\operatorname{coeff}(\operatorname{frobenius}(x),n) = (x_{n})^{p}.$$$$
Lean4
@[simp]
theorem coeff_frobenius_charP (x : 𝕎 R) (n : ℕ) : coeff (frobenius x) n = x.coeff n ^ p :=
by
rw [coeff_frobenius]
letI : Algebra (ZMod p) R :=
ZMod.algebra _
_
-- outline of the calculation, proofs follow below
calc
aeval (fun k => x.coeff k) (frobeniusPoly p n) =
aeval (fun k => x.coeff k) (MvPolynomial.map (Int.castRingHom (ZMod p)) (frobeniusPoly p n)) :=
?_
_ = aeval (fun k => x.coeff k) (X n ^ p : MvPolynomial ℕ (ZMod p)) := ?_
_ = x.coeff n ^ p := ?_
· conv_rhs => rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
apply eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
· rw [frobeniusPoly_zmod]
· rw [map_pow, aeval_X]
