addressing comment by Pierre

CHANGELOG_UNRELEASED.md

@@ -10,6 +10,9 @@
   + lemma `derive_cst`
   + lemma `deriveMr`, `deriveMl`
 
+- in `functions.v`:
+  + lemmas `mull_funE`, `mulr_funE`
+
 ### Changed
 
 ### Renamed

classical/functions.v

@@ -2617,6 +2617,14 @@ Lemma fct_sumE (I T : Type) (M : zmodType) r (P : {pred I}) (f : I -> T -> M)
   (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
 Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed.
 
+Lemma mull_funE (T : Type) {R : comSemiRingType} (f : T -> R) (r : R) :
+  r \*o f = r \o* f.
+Proof. by apply/funext => x/=; rewrite mulrC. Qed.
+
+Lemma mulr_funE (T : Type) {R : comSemiRingType} (f : T -> R) (r : R) :
+  r \o* f = r \*o f.
+Proof. by rewrite mull_funE. Qed.
+
 End function_space.
 
 Section function_space_lemmas.

theories/derive.v

@@ -1300,18 +1300,15 @@ exact: der_mult.
 Qed.
 
 Lemma deriveMr f (r : R) (x v : V) :
-  derivable f x v -> 'D_v (fun x => f x * r) x = (r * 'D_v f x)%R.
+  derivable f x v -> 'D_v (r \o* f) x = (r * 'D_v f x)%R.
 Proof.
 move/deriveM => /(_ _ (derivable_cst _ _ _)) ->.
 by rewrite derive_cst scaler0 add0r.
 Qed.
 
 Lemma deriveMl f (r : R) (x v : V) :
-  derivable f x v -> 'D_v (fun x => r * f x) x = (r * 'D_v f x)%R.
-Proof.
-move=> fxv.
-by rewrite -deriveMr//; under eq_fun do rewrite mulrC.
-Qed.
+  derivable f x v -> 'D_v (r \*o f) x = (r * 'D_v f x)%R.
+Proof. by move=> fxv; rewrite -deriveMr// mulr_funE. Qed.
 
 Global Instance is_deriveM f g (x v : V) (df dg : R) :
   is_derive x v f df -> is_derive x v g dg ->