Derivative_of_Function_of_Constant_Multiple

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

differential-calculusproofwiki

Let $f$ be a real function which is differentiable on $\R$ . Let $c \in \R$ be a constant. Then $\map {D_x} {\map f {c x} } = c \map {D_{c x} } {\map f {c x} }$

Preamble

import Mathlib.Analysis.Calculus.Deriv.Basic

Formal statement

theorem Derivative_of_Function_of_Constant_Multiple (f : ℝ → ℝ) (c x : ℝ) (hf : DifferentiableAt ℝ f x) : HasDerivAt (fun x => c * f x) (c * deriv f x) x := by sorry

Source

https://proofwiki.org/wiki/Derivative_of_Function_of_Constant_Multiple

View graph