English
The nth coefficient of the product p q is the sum, over all pairs (i,j) with i+j=n, of the product of the i-th coefficient of p and the j-th coefficient of q.
Русский
Коэффициент произведения p q на степени n равен сумме по всем парам (i,j) с i+j=n от p_i q_j.
LaTeX
$$$\operatorname{coeff}(p q) n = \sum_{x \in \operatorname{antidiagonal} n} \operatorname{coeff}(p, x.1) \cdot \operatorname{coeff}(q, x.2)$$$
Lean4
/-- Decomposes the coefficient of the product `p * q` as a sum
over `antidiagonal`. A version which sums over `range (n + 1)` can be obtained
by using `Finset.Nat.sum_antidiagonal_eq_sum_range_succ`. -/
theorem coeff_mul (p q : R[X]) (n : ℕ) : coeff (p * q) n = ∑ x ∈ antidiagonal n, coeff p x.1 * coeff q x.2 :=
by
rcases p with ⟨p⟩; rcases q with ⟨q⟩
simp_rw [← ofFinsupp_mul, coeff]
exact AddMonoidAlgebra.mul_apply_antidiagonal p q n _ Finset.mem_antidiagonal
