English
There are rational polynomials in the coefficients of a Witt vector that express the nth coefficient of Frobenius(x) in terms of the coefficients of x.
Русский
Существуют рациональные многочлены по коэффициентам Witt-вектора, которые выражают n-й коэффициент Frobenius(x) через коэффициенты x.
LaTeX
$$$\forall n \in \mathbb{N},\; \text{coeff}(\operatorname{frobenius}(x),n) = \mathrm{aeval}_{x.coeff}(\operatorname{frobeniusPoly(p,n)}).$$$
Lean4
/-- The rational polynomials that give the coefficients of `frobenius x`,
in terms of the coefficients of `x`.
These polynomials actually have integral coefficients,
see `frobeniusPoly` and `map_frobeniusPoly`. -/
def frobeniusPolyRat (n : ℕ) : MvPolynomial ℕ ℚ :=
bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1) (xInTermsOfW p ℚ n)
