wittNSMul — Mathlib

English

The polynomials for repeated addition by a natural number are given by wittNSMul p n = wittStructureInt p (n • X0).

Русский

Полиномы для повторного сложения на натуральное число: wittNSMul p n = wittStructureInt p (n • X0).

LaTeX

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

Lean4

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

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