feat(analysis/calculus/fderiv): generalize const_smul lemmas (#9399)

src/analysis/calculus/fderiv.lean

@@ -1397,46 +1397,49 @@ end prod_map
 end cartesian_product
 
 section const_smul
-/-! ### Derivative of a function multiplied by a constant -/
 
-theorem has_strict_fderiv_at.const_smul (h : has_strict_fderiv_at f f' x) (c : 𝕜) :
+variables {R : Type*} [semiring R] [module R F] [topological_space R] [smul_comm_class 𝕜 R F]
+  [has_continuous_smul R F]
+
+/-! ### Derivative of a function multiplied by a constant -/
+theorem has_strict_fderiv_at.const_smul (h : has_strict_fderiv_at f f' x) (c : R) :
   has_strict_fderiv_at (λ x, c • f x) (c • f') x :=
 (c • (1 : F →L[𝕜] F)).has_strict_fderiv_at.comp x h
 
-theorem has_fderiv_at_filter.const_smul (h : has_fderiv_at_filter f f' x L) (c : 𝕜) :
+theorem has_fderiv_at_filter.const_smul (h : has_fderiv_at_filter f f' x L) (c : R) :
   has_fderiv_at_filter (λ x, c • f x) (c • f') x L :=
 (c • (1 : F →L[𝕜] F)).has_fderiv_at_filter.comp x h
 
-theorem has_fderiv_within_at.const_smul (h : has_fderiv_within_at f f' s x) (c : 𝕜) :
+theorem has_fderiv_within_at.const_smul (h : has_fderiv_within_at f f' s x) (c : R) :
   has_fderiv_within_at (λ x, c • f x) (c • f') s x :=
 h.const_smul c
 
-theorem has_fderiv_at.const_smul (h : has_fderiv_at f f' x) (c : 𝕜) :
+theorem has_fderiv_at.const_smul (h : has_fderiv_at f f' x) (c : R) :
   has_fderiv_at (λ x, c • f x) (c • f') x :=
 h.const_smul c
 
-lemma differentiable_within_at.const_smul (h : differentiable_within_at 𝕜 f s x) (c : 𝕜) :
+lemma differentiable_within_at.const_smul (h : differentiable_within_at 𝕜 f s x) (c : R) :
   differentiable_within_at 𝕜 (λy, c • f y) s x :=
 (h.has_fderiv_within_at.const_smul c).differentiable_within_at
 
-lemma differentiable_at.const_smul (h : differentiable_at 𝕜 f x) (c : 𝕜) :
+lemma differentiable_at.const_smul (h : differentiable_at 𝕜 f x) (c : R) :
   differentiable_at 𝕜 (λy, c • f y) x :=
 (h.has_fderiv_at.const_smul c).differentiable_at
 
-lemma differentiable_on.const_smul (h : differentiable_on 𝕜 f s) (c : 𝕜) :
+lemma differentiable_on.const_smul (h : differentiable_on 𝕜 f s) (c : R) :
   differentiable_on 𝕜 (λy, c • f y) s :=
 λx hx, (h x hx).const_smul c
 
-lemma differentiable.const_smul (h : differentiable 𝕜 f) (c : 𝕜) :
+lemma differentiable.const_smul (h : differentiable 𝕜 f) (c : R) :
   differentiable 𝕜 (λy, c • f y) :=
 λx, (h x).const_smul c
 
 lemma fderiv_within_const_smul (hxs : unique_diff_within_at 𝕜 s x)
-  (h : differentiable_within_at 𝕜 f s x) (c : 𝕜) :
+  (h : differentiable_within_at 𝕜 f s x) (c : R) :
   fderiv_within 𝕜 (λy, c • f y) s x = c • fderiv_within 𝕜 f s x :=
 (h.has_fderiv_within_at.const_smul c).fderiv_within hxs
 
-lemma fderiv_const_smul (h : differentiable_at 𝕜 f x) (c : 𝕜) :
+lemma fderiv_const_smul (h : differentiable_at 𝕜 f x) (c : R) :
   fderiv 𝕜 (λy, c • f y) x = c • fderiv 𝕜 f x :=
 (h.has_fderiv_at.const_smul c).fderiv