frobeniusPoly — Mathlib

English

The Frobenius polynomial frobeniusPoly(p,n) is the polynomial X_n^p plus p times frobeniusPolyAux(p,n) in the integer-coefficient Witt polynomial ring, giving the nth coefficient of Frobenius on Witt vectors.

Русский

Многочлен frobeniusPoly(p,n) равен X_n^p плюс p умножить на frobeniusPolyAux(p,n) и задаёт n-й коэффициент Frobenius на Witt-векторах.

LaTeX

$$$\operatorname{frobeniusPoly}(p,n) = X_n^p + C(p) \cdot \operatorname{frobeniusPolyAux}(p,n).$$$

Lean4

/-- The polynomials that give the coefficients of `frobenius x`,
in terms of the coefficients of `x`. -/
def frobeniusPoly (n : ℕ) : MvPolynomial ℕ ℤ :=
  X n ^ p + C (p : ℤ) * frobeniusPolyAux p n

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