derivative_neg

Mathlib.Algebra.Polynomial.Derivative

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

English

For any polynomial f, the derivative of −f equals the negation of the derivative of f.

Русский

Для любого многочлена f производная от −f равна − производной f.

LaTeX

$$$\operatorname{derivative}(-f) = -\operatorname{derivative}f$$$

Lean4

@[simp]
theorem derivative_neg (f : R[X]) : derivative (-f) = -derivative f :=
  LinearMap.map_neg derivative f

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

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

Разделы

Аффилиация

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