totalDegree_le_of_support_subset

Mathlib.Algebra.MvPolynomial.Degrees

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

English

If q.totalDegree < p.totalDegree, then (p + q).totalDegree = p.totalDegree.

Русский

Если q.totalDegree < p.totalDegree, то (p+q).totalDegree = p.totalDegree.

LaTeX

$$$q.totalDegree < p.totalDegree \Rightarrow (p+q).totalDegree = p.totalDegree$$$

Lean4

theorem totalDegree_le_of_support_subset (h : p.support ⊆ q.support) : totalDegree p ≤ totalDegree q :=
  Finset.sup_mono h

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

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

Разделы

Аффилиация

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