coeff_frobeniusFun — Mathlib

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]

Похожие утверждения