nsmul_coeff — Mathlib

English

Let m be a natural number and x a Witt vector over R. The n-th coefficient of m • x equals the evaluation of the Witt polynomial wittNSMul p m n at the single coefficient sequence [x.coeff].

Русский

Пусть m целое и x — Witt-вектор над R. n-й коэффициент m • x равен значению полинома Витта wittNSMul p m n при единичной последовательности коэффициентов [x.coeff].

LaTeX

$$$(m \cdot x).\text{coeff } n = \operatorname{peval}(\operatorname{wittNSMul}(p,m,n), ![x.coeff])$$$

Lean4

theorem nsmul_coeff (m : ℕ) (x : 𝕎 R) (n : ℕ) : (m • x).coeff n = peval (wittNSMul p m n) ![x.coeff] := by
  simp [(· • ·), SMul.smul, eval, Matrix.cons_fin_one]

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