totalDegree_add

Mathlib.Algebra.MvPolynomial.Degrees

URI: https://scilib.ai/kg/mathlib#MvPolynomial.totalDegree_add

English

If c ≠ 0, then the total degree of monomial s with coefficient c is sum of exponents: totalDegree(monomial s c) = sum s.

Русский

Если c ≠ 0, то totalDegree(monomial s c) = ∑ s_i.

LaTeX

$$$\operatorname{totalDegree}(\mathrm{monomial}(s,c)) = \sum_i s_i \quad(\text{when } c \neq 0)$$$

Lean4

theorem totalDegree_add (a b : MvPolynomial σ R) : (a + b).totalDegree ≤ max a.totalDegree b.totalDegree :=
  sup_support_add_le _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru