neg_coeff — Mathlib

English

Let x be a Witt vector over R and n a natural number. The n-th coefficient of the negation of x is obtained by evaluating the Witt polynomial wittNeg p n at the single coefficient sequence [x.coeff].

Русский

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

LaTeX

$$$(-x).\text{coeff } n = \operatorname{peval}(\operatorname{wittNeg}(p,n), ![x.coeff])$$$

Lean4

theorem neg_coeff (x : 𝕎 R) (n : ℕ) : (-x).coeff n = peval (wittNeg p n) ![x.coeff] := by
  simp [Neg.neg, eval, Matrix.cons_fin_one]

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