English
Coefficient of p · X_s at m is 0 unless s ∈ support(m); if s ∈ m.support then it equals coeff(m − δ_s) p.
Русский
Коэффициент при p · X_s в m равен 0, если s не принадлежит опоре m; если же s ∈ support(m), то равен coeff(m − δ_s) p.
LaTeX
$$$\\operatorname{coeff}_m(p \\cdot X_s) = \\begin{cases} \\operatorname{coeff}_{m - \\delta_s} p & \\text{если } s \\in m.\\text{support}, \\\\ 0 & \\text{иначе} \\end{cases}$$$
Lean4
theorem coeff_mul_X' [DecidableEq σ] (m) (s : σ) (p : MvPolynomial σ R) :
coeff m (p * X s) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0 :=
by
refine (coeff_mul_monomial' _ _ _ _).trans ?_
simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero, mul_one]
