neg'

Mathlib.Analysis.Calculus.Deriv.Add

URI: https://scilib.ai/kg/mathlib#deriv.neg'

English

The derivative of -f is the function x ↦ - f'(x); i.e., (-f)' = - f'.

Русский

Производная от -f равна функции x ↦ - f'(x); то есть (-f)' = - f'.

LaTeX

$$$ (-f)' = - f' $$$

Lean4

@[simp]
theorem neg' : (deriv (-f)) = fun x ↦ -deriv f x :=
  deriv.fun_neg'

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

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

Разделы

Аффилиация

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