instMul — Mathlib

English

The coefficient at n of the product φ ⋅ ψ is the sum, over all pairs (p, q) with p + q = n, of coeff p φ times coeff q ψ.

Русский

Коэффициент в n от произведения φ и ψ равен сумме по всем парам (p, q) с p + q = n от произведения коэффициентов: coeff p φ · coeff q ψ.

LaTeX

$$$$ \\operatorname{coeff}_{n}(\\phi \\cdot \\psi) = \\sum_{p \\in \\operatorname{antidiagonal}(n)} \\operatorname{coeff}_{p.1}(\\phi) \\cdot \\operatorname{coeff}_{p.2}(\\psi). $$$$

Lean4

instance : Mul (MvPowerSeries σ R) :=
  letI := Classical.decEq σ
  ⟨fun φ ψ n => ∑ p ∈ antidiagonal n, coeff p.1 φ * coeff p.2 ψ⟩

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