coeff_C_mul — Mathlib

English

Coefficient of a product decomposes via antidiagonal: coeff n (p q) equals sum over antidiagonal n of coeff x.1 p · coeff x.2 q.

Русский

Коэффициент произведения распадается по антидиагонали: coeff n (p q) = ∑ x в antidiagonal n, coeff x.1 p · coeff x.2 q.

LaTeX

$$$\mathrm{coeff}\ n (p q) =\ \sum_{x \in \mathrm{Finset}.\mathrm{antidiagonal}\ n} \mathrm{coeff}\ x.1\ p \cdot \mathrm{coeff}\ x.2\ q$$$

Lean4

@[simp]
theorem coeff_C_mul (m) (a : R) (p : MvPolynomial σ R) : coeff m (C a * p) = a * coeff m p := by
  classical
  rw [mul_def, sum_C]
  · simp +contextual [sum_def, coeff_sum]
  simp

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