deriv_sub_const_fun — Mathlib

English

For any c, the derivative of the function y ↦ f(y) − c is equal to the derivative of f, i.e., deriv (f − c) = deriv f.

Русский

Для любой константы c производная функции y ↦ f(y) − c равна производной f, то есть deriv (f − c) = deriv f.

LaTeX

$$$$ \operatorname{deriv}(f - c) x = \operatorname{deriv} f x. $$$$

Lean4

@[simp]
theorem deriv_sub_const_fun (c : F) : deriv (f · - c) = deriv f :=
  by
  ext
  apply deriv_sub_const

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