degrees_mul_le

Mathlib.Algebra.MvPolynomial.Degrees

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

← MathLib Explorer

English

For polynomials p, q, deg(p q) ≤ deg(p) ⊔ deg(q).

Русский

Для многочленов p, q верно deg(p q) ≤ deg(p) ⊔ deg(q).

LaTeX

$$$\deg(p q) \le \deg(p) \sqcup \deg(q)$$$

Lean4

theorem degrees_mul_le {p q : MvPolynomial σ R} : (p * q).degrees ≤ p.degrees + q.degrees := by
  classical
  simp_rw [degrees_def]
  exact supDegree_mul_le (map_add _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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