wittPow — Mathlib

English

The polynomials describing taking powers in 𝕎R are given by wittPow p (n) = wittStructureInt p (X0^n).

Русский

Полиномы для возведения в степень в 𝕎R: wittPow p (n) = wittStructureInt p (X0^n).

LaTeX

$$$\\mathrm{WittVector.wittPow}(p)(n) = wittStructureInt(p, X_0^{n})$$$

Lean4

/-- The polynomials used for defining repeated addition of the ring of Witt vectors. -/
def wittPow (n : ℕ) : ℕ → MvPolynomial (Fin 1 × ℕ) ℤ :=
  wittStructureInt p (X 0 ^ n)

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