coeff_neg — Mathlib

English

For every index m, the coefficient of −p at m equals the negation of the coefficient of p at m.

Русский

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

LaTeX

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

Lean4

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

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