add_coeff — Mathlib

English

For x,y in 𝕎 R and n ∈ ℕ, the nth coefficient of x+y equals peval(wittAdd(p,n)) applied to the pair of coefficients.

Русский

Для x,y ∈ 𝕎 R и n ∈ ℕ, коэффициент n суммы x+y равен применения к паре коэффициентов функции Witt-add: peval(wittAdd(p,n)).

LaTeX

$$$$ (x+y).\mathrm{coeff}\,n = \mathrm{peval}\big(\mathrm{wittAdd}(p,n)\big)(![x.\mathrm{coeff}, y.\mathrm{coeff}]). $$$$

Lean4

theorem add_coeff (x y : 𝕎 R) (n : ℕ) : (x + y).coeff n = peval (wittAdd p n) ![x.coeff, y.coeff] := by
  simp [(· + ·), Add.add, eval]

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