coeff_sub — Mathlib

English

For every index m, the coefficient at m of p − q is the difference of the coefficients of p and q at m.

Русский

Для каждого индекса m коэффициент над p − q равен разности коэффициентов над p и q при m.

LaTeX

$$$\\mathrm{coeff}\\, m\\lbrack p - q \\rbrack = \\mathrm{coeff}\\, m\\lbrack p \\rbrack - \\mathrm{coeff}\\, m\\lbrack q \\rbrack$$$

Lean4

@[simp]
theorem coeff_sub (m : σ →₀ ℕ) (p q : MvPolynomial σ R) : coeff m (p - q) = coeff m p - coeff m q :=
  Finsupp.sub_apply _ _ _

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