deriv_neg''

Mathlib.Analysis.Calculus.Deriv.Add

URI: https://scilib.ai/kg/mathlib#deriv_neg''

English

The derivative of the function x ↦ -x at x is −1; i.e., deriv (−x) (x) = −1.

Русский

Производная функции x ↦ −x в точке x равна −1; то есть deriv (−x) (x) = −1.

LaTeX

$$$ \dfrac{d}{dt}(-t)\big|_{t=x} = -1 $$$

Lean4

@[simp]
theorem deriv_neg'' : deriv (fun x : 𝕜 ↦ -x) x = -1 :=
  deriv_neg x

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

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

Разделы

Аффилиация

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