English
Another formulation of the product coefficient expansion using antidiagonal, identical in content to the previous statement.
Русский
Еще одна формулировка того же разложения коэффициентов произведения по антидиагонали.
LaTeX
$$$\mathrm{coeff}\ n (p q) =\ \sum_{x \in \mathrm{antidiagonal}\ n} \mathrm{coeff}\ x.1\ p \cdot \mathrm{coeff}\ x.2\ q$$$
Lean4
theorem coeff_mul [DecidableEq σ] (p q : MvPolynomial σ R) (n : σ →₀ ℕ) :
coeff n (p * q) = ∑ x ∈ Finset.antidiagonal n, coeff x.1 p * coeff x.2 q :=
AddMonoidAlgebra.mul_apply_antidiagonal p q _ _ Finset.mem_antidiagonal