coeff_mul — Mathlib

English

The coefficient at n of the product φ ⋅ monomial n a is the sum over p with p + n = m, giving a times coeff (m − n) φ when appropriate.

Русский

Коэффициент в n от произведения φ и мономиала с индексом n и коэффициентом a равен a ⋅ coeff_{n−p}(φ) суммированному по подходящим p.

LaTeX

$$$$ \\operatorname{coeff}_{m}(\\phi \\cdot \\operatorname{monomial}(n, a)) = \\begin{cases} a \\cdot \\operatorname{coeff}_{m-n}(\\phi), & n \\le m \\ \\ 0, & \\text{otherwise} \\end{cases} $$$$

Lean4

theorem coeff_mul [DecidableEq σ] : coeff n (φ * ψ) = ∑ p ∈ antidiagonal n, coeff p.1 φ * coeff p.2 ψ :=
  by
  refine Finset.sum_congr ?_ fun _ _ => rfl
  rw [Subsingleton.elim (Classical.decEq σ) ‹DecidableEq σ›]

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