deriv_const_add'

Mathlib.Analysis.Calculus.Deriv.Add

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

English

The derivative of a function with a constant added on the left equals the derivative of the function itself.

Русский

Производная от константы слева к функции равна производной самой функции.

LaTeX

$$$(\text{deriv} \; (c + f)) = \text{deriv} f$$$

Lean4

@[simp]
theorem deriv_const_add' (c : F) : (deriv (c + f ·)) = deriv f :=
  funext fun _ ↦ deriv_const_add c

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

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

Разделы

Аффилиация

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