wittZSMul — Mathlib

English

The polynomials for integer scaling of Witt vectors are given by wittZSMul p (n) = wittStructureInt p (n • X0).

Русский

Полиномы для целочисленного масштабирования Witt‑векторов: wittZSMul p n = wittStructureInt p (n • X0).

LaTeX

$$$\\mathrm{WittVector.wittZSMul}(p,n) = wittStructureInt(p, n \\cdot X_0)$$$

Lean4

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

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