mul_def — Mathlib

English

The multiplication in MvPolynomial expands as a double sum over exponents, combining monomials with exponents m+n and coefficients a*b.

Русский

Умножение в MvPolynomial раскладывается на двукратную сумму по степеням: мономиалы со степенями m+n и коэффициентами a*b.

LaTeX

$$$ p * q = \sum_{m,a} \sum_{n,b} \operatorname{monomial}(m+n)(a\cdot b) $$$

Lean4

theorem mul_def : p * q = p.sum fun m a => q.sum fun n b => monomial (m + n) (a * b) :=
  AddMonoidAlgebra.mul_def ..

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