deriv_fun_const_smul — Mathlib

English

Let f: 𝕜 → F be differentiable at x. For any scalar c in the base field, the derivative of y ↦ c · f(y) at x equals c · f'(x).

Русский

Пусть f: 𝕜 → F дифференцируема в точке x. Для любого скаляра c из основы поля производная функции y ↦ c · f(y) в точке x равна c · f'(x).

LaTeX

$$$\operatorname{deriv} \bigl(y \mapsto c \cdot f(y)\bigr)\!\,x = c \cdot \operatorname{deriv} f(x)$$$

Lean4

theorem deriv_fun_const_smul (c : R) (hf : DifferentiableAt 𝕜 f x) : deriv (fun y => c • f y) x = c • deriv f x :=
  (hf.hasDerivAt.const_smul c).deriv

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