mul_eq_sum_sum — Mathlib

English

The product p q can be expressed as a double sum over indices i and j, aggregating coefficients via monomials of degree i+j.

Русский

Произведение p q можно выразить как двойную сумму по индексам i и j, сводя коэффициенты к мономиалам степени i+j.

LaTeX

$$$ p q = \sum_{i \in p.support} q.sum \; (j,a) \mapsto \operatorname{monomial}(i+j)(p.coeff(i)\cdot a) $$$

Lean4

/-- Expressing the product of two polynomials as a double sum. -/
theorem mul_eq_sum_sum : p * q = ∑ i ∈ p.support, q.sum fun j a => (monomial (i + j)) (p.coeff i * a) :=
  by
  apply toFinsupp_injective
  simp_rw [sum, coeff, toFinsupp_sum, support, toFinsupp_mul, toFinsupp_monomial, AddMonoidAlgebra.mul_def, Finsupp.sum]

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