deriv_neg'

Mathlib.Analysis.Calculus.Deriv.Add

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

English

The derivative of the negation function at x is −1: deriv(−id)(x) = −1.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem deriv_neg' : deriv (Neg.neg : 𝕜 → 𝕜) = fun _ ↦ -1 :=
  funext deriv_neg

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

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

Разделы

Аффилиация

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