degree_mul_le_of_le

Mathlib.Algebra.Polynomial.Degree.Definitions

URI: https://scilib.ai/kg/mathlib#Polynomial.degree_mul_le_of_le

← MathLib Explorer

English

If deg p ≤ a and deg q ≤ b, then deg(p q) ≤ a + b.

Русский

Если deg p ≤ a и deg q ≤ b, то deg(p q) ≤ a + b.

LaTeX

$$$\deg(p q) \le a + b \text{ given } \deg(p) \le a \text{ and } \deg(q) \le b$$$

Lean4

theorem degree_mul_le_of_le {a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) : degree (p * q) ≤ a + b :=
  (p.degree_mul_le _).trans <| add_le_add ‹_› ‹_›

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

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

Разделы

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

Аффилиация

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