From bddc3934da05ee8f00b7ecdae7b03a4b9d8a45a5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 13 Aug 2025 11:37:54 +0900 Subject: [PATCH 1/2] fixes #1647 --- theories/derive.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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. From 9799b57579b2d14688c8b840ae9fea2efc3a5b3d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 13 Aug 2025 11:40:26 +0900 Subject: [PATCH 2/2] upd changelog --- CHANGELOG_UNRELEASED.md | 3 +++ 1 file changed, 3 insertions(+) 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`