English
Let c, d: 𝕜 → 𝔸 be differentiable within a set s at x with derivatives c', d'. Then the derivative within s of the product c(y) d(y) equals c'(x) d(x) + c(x) d'(x).
Русский
Пусть c, d: 𝕜 → 𝔸 дифференцируемы внутри множества s в точке x с производными c', d'. Тогда производная внутри s от произведения c(y) d(y) в точке x равна c'(x) d(x) + c(x) d'(x).
LaTeX
$$$\operatorname{derivWithin}(c \cdot d)\,s\,x = (\operatorname{derivWithin} c\,s\,x) \cdot d(x) + c(x) \cdot (\operatorname{derivWithin} d\,s\,x)$$$
Lean4
/-- A variant of `deriv_const_smul` without differentiability assumption when the scalar
multiplication is by field elements. -/
theorem deriv_const_smul' {f : 𝕜 → F} {x : 𝕜} {R : Type*} [Field R] [Module R F] [SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F] (c : R) : deriv (c • f) x = c • deriv f x := by
simp only [← derivWithin_univ, derivWithin_const_smul']
