degree_derivative_le

Mathlib.Algebra.Polynomial.Derivative

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

← MathLib Explorer

English

For any polynomial p, the degree of its derivative is at most the degree of p.

Русский

Для любого многочлена p deg(p') ≤ deg(p).

LaTeX

$$$\deg(p') \le \deg(p)$$$

Lean4

theorem degree_derivative_le {p : R[X]} : p.derivative.degree ≤ p.degree :=
  letI := Classical.decEq R
  if H : p = 0 then le_of_eq <| by rw [H, derivative_zero] else (degree_derivative_lt H).le

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

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

Разделы

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

Аффилиация

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