derivative_of_natDegree_zero

Mathlib.Algebra.Polynomial.Derivative

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

English

If a polynomial p has natDegree equal to 0, then its derivative is zero.

Русский

Если natDegree полинома p равно 0, то производная p равна 0.

LaTeX

$$$\\text{If } p\\text{ has } \\operatorname{natDegree}(p)=0\\text{, then } \\operatorname{derivative}(p)=0.$$$

Lean4

theorem derivative_of_natDegree_zero {p : R[X]} (hp : p.natDegree = 0) : derivative p = 0 := by
  rw [eq_C_of_natDegree_eq_zero hp, derivative_C]

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

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

Разделы

Аффилиация

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