English
Coefficient of p · X_s at m is the coefficient at m with s added if s already occurs in m; otherwise 0.
Русский
Коэффициент при p · X_s в m равен коэффициенту в m − δ_s, если δ_s присутствует в m; иначе 0.
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_X_mul' [DecidableEq σ] (m) (s : σ) (p : MvPolynomial σ R) :
coeff m (X s * p) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0 :=
by
refine (coeff_monomial_mul' _ _ _ _).trans ?_
simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero, one_mul]
