deriv_neg

Mathlib.Analysis.Calculus.Deriv.Add

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

English

The derivative of the negation at x equals −1; i.e., deriv(−id)(x) = −1.

Русский

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

LaTeX

$$$ (-\mathrm{id})'(x) = -1 $$$

Lean4

theorem deriv_neg : deriv Neg.neg x = -1 :=
  HasDerivAt.deriv (hasDerivAt_neg x)

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

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

Разделы

Аффилиация

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