From c3dad6390e65270c296b586e7cd84d2f47e27483 Mon Sep 17 00:00:00 2001
From: yosakaon <lynda.bentoucha@etu.u-paris.fr>
Date: Thu, 16 Jul 2026 19:38:17 +0200
Subject: [PATCH 1/3] is_derive_mulmx

---
 theories/derive.v | 30 +++++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

diff --git a/theories/derive.v b/theories/derive.v
index e62456e54d..6246fc41d4 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -2453,6 +2453,33 @@ pose gL : {linear _ -> _} := HB.pack g glM.
 by apply: (@diff_unique _ _ _ _ gL); have [? ?] := dmx dM.
 Qed.
 
+Global Instance is_derive_mx_coord n m
+    (f : V -> 'M[R]_(n, m)) (f' : 'M[R]_(n,m)) (t : V) w :
+  is_derive t w f f' ->
+  forall i j, is_derive t w (fun x => f x i j) (f' i j).
+Proof.
+move=> fD i j /=.
+have fDer : derivable f t w by case: fD.
+apply/DeriveDef; last by have [_ <-] := fD; rewrite derive_mx// mxE.
+  by move/derivable_mxP : fDer => /(_ i j).
+Qed.
+
+Global Instance is_derive_mulmx n m p
+    (M : V -> 'M[R]_(n, m)) M'
+    (N : V -> 'M[R]_(m, p)) N' (t : V) w :
+  is_derive t w M M'  -> is_derive t w N N' ->
+  is_derive t w (fun t => M t *m N t) ((M' *m N t) + (M t *m N')).
+Proof.
+move=> is_der_M' is_der_N'. 
+apply (@is_derive_mx ) => i j /=.
+rewrite !mxE /=.
+under eq_fun do rewrite mxE /=.
+rewrite -!big_split /= -fct_sumE.
+apply/is_derive_sum => j0.
+rewrite mulrC addrC.
+apply/is_deriveM.
+Qed.
+
 End pointwise_derive.
 
 Section Ris_diff_mx.
@@ -2474,9 +2501,10 @@ have [diffMij dMdM] := MdM i j.
 rewrite -deriveE//.
 move/(congr1 (fun f => f v)) : dMdM.
 rewrite -(deriveE _ diffMij) => <-.
-rewrite derive_mx ?mxE//=.
+rewrite derive_mx ?mxE /=.
 apply/derivable_mxP => i0 j0/=.
 by have [/diff_derivable-/(_ v)] := MdM i0 j0.
+done.
 Qed.
 
 End Ris_diff_mx.

From 1c824abeb5b98d1be71ac6948d92df1b893a4ecc Mon Sep 17 00:00:00 2001
From: yosakaon <lynda.bentoucha@etu.u-paris.fr>
Date: Fri, 17 Jul 2026 11:06:20 +0200
Subject: [PATCH 2/3] changelog edit

---
 CHANGELOG_UNRELEASED.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9d34c3bd5e..ad84339eaf 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -94,6 +94,9 @@
   + lemma `diffmx`
   + lemma `is_diff_mx`
   + instance `is_diff_mx`
+  + instance `is_derive_coord`
+  + instance `is_derive_mulmx`
+
 - in `realsum.v`:
   + lemma `esum_psum`
   + lemma `esum_sum`

From 442b6414dc27de1487161a50fa27efa0d234db1f Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 29 Jul 2026 11:04:19 +0900
Subject: [PATCH 3/3] nitpick

---
 theories/derive.v | 20 +++++++++-----------
 1 file changed, 9 insertions(+), 11 deletions(-)

diff --git a/theories/derive.v b/theories/derive.v
index 6246fc41d4..b3727b1587 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -2461,23 +2461,22 @@ Proof.
 move=> fD i j /=.
 have fDer : derivable f t w by case: fD.
 apply/DeriveDef; last by have [_ <-] := fD; rewrite derive_mx// mxE.
-  by move/derivable_mxP : fDer => /(_ i j).
+by move/derivable_mxP : fDer => /(_ i j).
 Qed.
 
 Global Instance is_derive_mulmx n m p
     (M : V -> 'M[R]_(n, m)) M'
     (N : V -> 'M[R]_(m, p)) N' (t : V) w :
   is_derive t w M M'  -> is_derive t w N N' ->
-  is_derive t w (fun t => M t *m N t) ((M' *m N t) + (M t *m N')).
+  is_derive t w (fun t => M t *m N t) (M' *m N t + M t *m N').
 Proof.
-move=> is_der_M' is_der_N'. 
-apply (@is_derive_mx ) => i j /=.
-rewrite !mxE /=.
-under eq_fun do rewrite mxE /=.
+move=> is_der_M' is_der_N'.
+apply is_derive_mx => i j /=.
+rewrite !mxE/=.
+under eq_fun do rewrite mxE/=.
 rewrite -!big_split /= -fct_sumE.
-apply/is_derive_sum => j0.
-rewrite mulrC addrC.
-apply/is_deriveM.
+apply/is_derive_sum => k.
+by rewrite mulrC addrC; exact/is_deriveM.
 Qed.
 
 End pointwise_derive.
@@ -2501,10 +2500,9 @@ have [diffMij dMdM] := MdM i j.
 rewrite -deriveE//.
 move/(congr1 (fun f => f v)) : dMdM.
 rewrite -(deriveE _ diffMij) => <-.
-rewrite derive_mx ?mxE /=.
+rewrite derive_mx; last by rewrite /= mxE.
 apply/derivable_mxP => i0 j0/=.
 by have [/diff_derivable-/(_ v)] := MdM i0 j0.
-done.
 Qed.
 
 End Ris_diff_mx.