coeff_mul_X — Mathlib

English

Coefficient after multiplying by X_i is given by coeff (m + single i 1) (p * X_i) = coeff m p.

Русский

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

LaTeX

$$$\mathrm{coeff}\ (m + \mathrm{single}\ i\ 1)\big(p \cdot X_i\big) = \mathrm{coeff}\ m\ p$$$

Lean4

@[simp]
theorem coeff_mul_X (m) (s : σ) (p : MvPolynomial σ R) : coeff (m + Finsupp.single s 1) (p * X s) = coeff m p :=
  (coeff_mul_monomial _ _ _ _).trans (mul_one _)

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