English
For φ, ψ ∈ R⟦X⟧, the n-th coefficient of φψ equals the sum over antidiagonal n of coeff p.1 φ · coeff p.2 ψ.
Русский
Для φ, ψ ∈ R⟦X⟧, n-й коэффициент произведения φψ равен сумме по антидиагонали n коэффициентов φ и ψ.
LaTeX
$$$\operatorname{coeff}_n(\varphi \cdot \psi) = \sum_{p\in \operatorname{antidiagonal} n} \operatorname{coeff}_{p.1}(\varphi) \cdot \operatorname{coeff}_{p.2}(\psi)$$$
Lean4
theorem coeff_mul (n : ℕ) (φ ψ : R⟦X⟧) : coeff n (φ * ψ) = ∑ p ∈ antidiagonal n, coeff p.1 φ * coeff p.2 ψ := by
-- `rw` can't see that `PowerSeries = MvPowerSeries Unit`, so use `.trans`
refine (MvPowerSeries.coeff_mul _ φ ψ).trans ?_
rw [Finsupp.antidiagonal_single, Finset.sum_map]
rfl
