support_mul — Mathlib

English

For a finite-support monomial with nonzero coefficient, the total degree equals the sum of the exponents in the monomial.

Русский

Для мономиала с конечной опорой и ненулевой коэффициентом общая степень равна сумме степеней по всем индексам.

LaTeX

$$$\operatorname{totalDegree}(\operatorname{monomial}(s)\; c) = \sum_{i} s(i)\;$ (для $c \ne 0$)$$

Lean4

theorem support_mul [DecidableEq σ] (p q : MvPolynomial σ R) : (p * q).support ⊆ p.support + q.support :=
  AddMonoidAlgebra.support_mul p q

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