coeff_mul — Mathlib

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

Похожие утверждения