English
A natural-indexed version of monomial_smul_apply holds for natural indices.
Русский
Версия мононимиального smul_apply с натуральными индексами.
LaTeX
$$monomial_smul_apply (i : Nat) (r : R) (j : Nat) (m : M) = single R (i + j) (r • m)$$
Lean4
theorem smul_apply (f : R[X]) (g : PolynomialModule R M) (n : ℕ) :
(f • g) n = ∑ x ∈ Finset.antidiagonal n, f.coeff x.1 • g x.2 := by
induction f using Polynomial.induction_on' with
| add p q hp hq =>
rw [add_smul, Finsupp.add_apply, hp, hq, ← Finset.sum_add_distrib]
congr
ext
rw [coeff_add, add_smul]
| monomial f_n
f_a =>
rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j => (monomial f_n f_a).coeff i • g j, monomial_smul_apply]
simp_rw [Polynomial.coeff_monomial, ← Finset.mem_range_succ_iff]
simp
