diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9f96f5d862..78d0bf711e 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -77,6 +77,9 @@
   + `ltr_expeR` -> `lte_expeR`
   + `ler_expeR` -> `lee_expeR`
 
+- in `derive.v`:
+  + `derivemxE` -> `deriveEjacobian`
+
 ### Generalized
 
 - in `functions.v`
diff --git a/theories/derive.v b/theories/derive.v
index 5362d57f99..3e9e0608fd 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -353,7 +353,7 @@ Section DifferentialR2.
 Variable R : numFieldType.
 Implicit Type (V : normedModType R).
 
-Lemma derivemxE m n (f : 'rV[R]_m.+1 -> 'rV[R]_n.+1) (a v : 'rV[R]_m.+1) :
+Lemma deriveEjacobian m n (f : 'rV[R]_m.+1 -> 'rV[R]_n.+1) (a v : 'rV[R]_m.+1) :
   differentiable f a -> 'D_ v f a = v *m jacobian f a.
 Proof. by move=> /deriveE->; rewrite /jacobian mul_rV_lin1. Qed.
 
@@ -390,9 +390,10 @@ Lemma derive1Sn V (f : R -> V) n : f^`(n.+1) = f^`()^`(n).
 Proof. exact: iterSr. Qed.
 
 End DifferentialR2.
-
 Notation "f ^` ()" := (derive1 f) : classical_set_scope.
 Notation "f ^` ( n )" := (derive1n n f) : classical_set_scope.
+#[deprecated(since="mathcomp-analysis 1.13.0", note="renamed to `deriveEjacobian`")]
+Notation derivemxE := deriveEjacobian (only parsing).
 
 Section DifferentialR3.
 Variable R : numFieldType.