English
The coefficient at m of the product monomial n a ⋅ φ is if n ≤ m then a ⋅ coeff_{m−n} φ else 0.
Русский
Коэффициент в m от произведения мономиала n a и φ равен 0, если n > m; иначе равен a ⋅ coeff_{m−n} φ.
LaTeX
$$$$ \\operatorname{coeff}_{m}(\\operatorname{monomial}(n, a) \\cdot \\phi) = \\begin{cases} a \\cdot \\operatorname{coeff}_{m-n} \\phi, & n \\le m \\ 0, & \\text{otherwise} \\end{cases} $$$$
Lean4
theorem coeff_monomial_mul (a : R) : coeff m (monomial n a * φ) = if n ≤ m then a * coeff (m - n) φ else 0 := by
classical
have : ∀ p ∈ antidiagonal m, coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial n a) * coeff p.2 φ ≠ 0 → p.1 = n :=
fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp)
rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_fst_eq_antidiagonal _ n, Finset.sum_ite_index]
simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]
