deriv_const_add

Mathlib.Analysis.Calculus.Deriv.Add

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

English

The derivative of f plus a constant is the derivative of f: deriv (f + c) x = deriv f x.

Русский

Производная от f плюс константа равна производной f.

LaTeX

$$$\ deriv (f + c) x = deriv f x$$$

Lean4

theorem deriv_const_add (c : F) : deriv (c + f ·) x = deriv f x := by simp only [deriv, fderiv_const_add]

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

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

Разделы

Аффилиация

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