English
For a fixed scalar c in a field and any function f, the derivative at x of y ↦ c · f(y) equals c times the derivative of f at x, with no extra differentiability assumption on c.
Русский
Пусть фиксированный скаляр c принадлежит полю; производная функции y ↦ c · f(y) в точке x равна c · f'(x), без дополнительных предположений о дифференцируемости c.
LaTeX
$$$\operatorname{deriv} (y \mapsto c \cdot f(y)) \\ x = c \cdot \operatorname{deriv} f(x)$$$
Lean4
/-- A variant of `deriv_const_smul` without differentiability assumption when the scalar
multiplication is by field elements. -/
theorem deriv_fun_const_smul' {f : 𝕜 → F} {x : 𝕜} {R : Type*} [Field R] [Module R F] [SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F] (c : R) : deriv (fun y ↦ c • f y) x = c • deriv f x := by
simp only [← derivWithin_univ, derivWithin_fun_const_smul']
