English
Let p be a multivariate polynomial over a commutative semiring R and s an index in σ. For every finite support exponent m ∈ σ →₀ ℕ, the coefficient of X_s · p at the exponent m is equal to the coefficient of p at the exponent m − 0 with the s-component increased by 1; equivalently, coeff at m with X_s p equals coeff at m with p when the index is shifted by s.
Русский
Пусть p — многочлен в переменных σ над коммутативным кольцом R, и пусть s ∈ σ. Для любого мультииндекса m ∈ σ →₀ ℕ коэффициент при X_s · p с экспонентой m равен коэффициенту p с экспонентой m, когда добавляют к индексу единицу в координате s.
LaTeX
$$$\\operatorname{coeff}(Finsupp.single s 1 + m)\\bigl(X s \\cdot p\\bigr) = \\operatorname{coeff} m\\,p$$$
Lean4
@[simp]
theorem coeff_X_mul (m) (s : σ) (p : MvPolynomial σ R) : coeff (Finsupp.single s 1 + m) (X s * p) = coeff m p :=
(coeff_monomial_mul _ _ _ _).trans (one_mul _)
