sub_coeff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sub_coeff (x y : 𝕎 R) (n : ℕ) : (x - y).coeff n = peval (wittSub p n) ![x.coeff, y.coeff] := by
  simp [(· - ·), Sub.sub, eval]

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