natDegree_derivative_le

Mathlib.Algebra.Polynomial.Derivative

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

← MathLib Explorer

English

For any p, natDegree(p') ≤ natDegree(p) − 1 (where natDegree is defined).

Русский

Для любого p natDegree(p') ≤ natDegree(p) − 1.

LaTeX

$$$\text{natDegree}(p') \le \text{natDegree}(p) - 1$$$

Lean4

theorem natDegree_derivative_le (p : R[X]) : p.derivative.natDegree ≤ p.natDegree - 1 :=
  by
  by_cases p0 : p.natDegree = 0
  · simp [p0, derivative_of_natDegree_zero]
  · exact Nat.le_sub_one_of_lt (natDegree_derivative_lt p0)

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

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

Разделы

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

Аффилиация

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