English
Coefficient of p · monomial(s, r) at m equals coeff(m − s) p · r when s ≤ m, otherwise 0.
Русский
Коэффициент при p · мономиал(s, r) с экспонентой m равен coeff(m − s) p · r при s ≤ m, иначе 0.
LaTeX
$$$\\operatorname{coeff}_m(p \\cdot \\mathrm{monomial}(s, r)) = \\begin{cases} \\operatorname{coeff}_{m - s} p \\cdot r & \\text{если } s \\le m, \\\\ 0 & \\text{иначе} \\end{cases}$$$
Lean4
theorem coeff_mul_monomial' (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) :
coeff m (p * monomial s r) = if s ≤ m then coeff (m - s) p * r else 0 := by
classical
split_ifs with h
· conv_rhs => rw [← coeff_mul_monomial _ s]
rw [tsub_add_cancel_of_le h]
· contrapose! h
rw [← mem_support_iff] at h
obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
simpa [Finset.mem_add] using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h
exact le_add_left le_rfl
