English
Coefficient of monomial(s) · p times monomial s with coefficient r on the left is given by the same rule as above with r moved to the front.
Русский
Коэффициент при мономиале(s) · p слева записывается по аналогичному правилу с коэффициентом r впереди.
LaTeX
$$$\\operatorname{coeff}_m(\\mathrm{monomial}(s, r) \\cdot p) = \\begin{cases} r \\cdot \\operatorname{coeff}_{m - s} p & \\text{если } s \\le m, \\\\ 0 & \\text{иначе} \\end{cases}$$$
Lean4
theorem coeff_monomial_mul' (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) :
coeff m (monomial s r * p) = if s ≤ m then r * coeff (m - s) p else 0 := by
-- note that if we allow `R` to be non-commutative we will have to duplicate the proof above.
rw [mul_comm, mul_comm r]
exact coeff_mul_monomial' _ _ _ _
