zsmul_coeff — Mathlib

English

Let m be an integer and x a Witt vector over R. The n-th coefficient of m • x equals the evaluation of the Witt polynomial wittZSMul p m n at [x.coeff].

Русский

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

LaTeX

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

Lean4

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

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