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