coeff_add — Mathlib

English

The coefficient at m of a sum equals the sum of the coefficients: coeff m (p+q) = coeff m p + coeff m q.

Русский

Коэффициент при m суммы равен сумме коэффициентов: coeff_m(p+q) = coeff_m(p) + coeff_m(q).

LaTeX

$$$\forall m\ p,q:\ \mathrm{coeff}\;m (p+q) = \mathrm{coeff}\;m\;p + \mathrm{coeff}\;m\;q$$$

Lean4

@[simp]
theorem coeff_add (m : σ →₀ ℕ) (p q : MvPolynomial σ R) : coeff m (p + q) = coeff m p + coeff m q :=
  add_apply p q m

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