English
For a Witt vector x and n, the nth coefficient of FrobeniusFun(x) equals the evaluation of FrobeniusPoly(p,n) on the coefficients of x.
Русский
Для Witt-вектора x и индекса n, n-й коэффициент FrobeniusFun(x) равен значению FrobeniusPoly(p,n) на коэффициентах x.
LaTeX
$$$\text{coeff}(\operatorname{frobeniusFun}(x),n) = \mathrm{aeval}_{x.coeff}(\operatorname{frobeniusPoly}(p,n)).$$$
Lean4
theorem coeff_frobeniusFun (x : 𝕎 R) (n : ℕ) :
coeff (frobeniusFun x) n = MvPolynomial.aeval x.coeff (frobeniusPoly p n) := by rw [frobeniusFun, coeff_mk]