From fdb3e889be8fcf1cad68e1e17e198150c7b03e91 Mon Sep 17 00:00:00 2001
From: yosakaon <lynda.bentoucha@etu.u-paris.fr>
Date: Fri, 31 Jul 2026 08:18:34 +0200
Subject: [PATCH] hint is_derive_mulmx

---
 theories/derive.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/derive.v b/theories/derive.v
index b3727b1587..77bd95cf04 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -2481,6 +2481,8 @@ Qed.
 
 End pointwise_derive.
 
+#[global] Hint Extern 0 (is_derive _ _ (fun x => _ *m _) _) => apply: is_derive_mulmx : typeclass_instances.
+
 Section Ris_diff_mx.
 Local Open Scope classical_set_scope.
 Context {R : realFieldType}.