coeff_monomial_mul — Mathlib

English

Coefficient after multiplying by a monomial scales by the monomial's coefficient: coeff (m+s) (p * monomial s r) = coeff m p · r.

Русский

После умножения на мономиал коэффициент при m+s равняется коэффициенту p при m, умноженному на r.

LaTeX

$$$\mathrm{coeff}(m+s)\big(p \cdot \mathrm{monomial}(s,r)\big) = \mathrm{coeff}(m, p) \cdot r$$$

Lean4

@[simp]
theorem coeff_monomial_mul (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) :
    coeff (s + m) (monomial s r * p) = r * coeff m p :=
  AddMonoidAlgebra.single_mul_apply_aux fun _a _ => add_right_inj _

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