pow_coeff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem pow_coeff (m : ℕ) (x : 𝕎 R) (n : ℕ) : (x ^ m).coeff n = peval (wittPow p m n) ![x.coeff] := by
  simp [(· ^ ·), Pow.pow, eval, Matrix.cons_fin_one]

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