From 40b876679857e2651686a7940c105c937b217e04 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 6 Aug 2026 23:35:42 +0900 Subject: [PATCH] making is_derive_mx instance causes loops --- theories/derive.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/derive.v b/theories/derive.v index 33b99954aa..928314dc33 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -2408,7 +2408,7 @@ rewrite (le_trans (ler_normD _ _))// (splitr e) lerD//. by rewrite sub0r normrN; near: x; exact: dnbhs0_lt. Unshelve. all: by end_near. Qed. -Global Instance is_derive_mx {m n : nat} (M : V -> 'M[R]_(m, n)) +Lemma is_derive_mx {m n : nat} (M : V -> 'M[R]_(m, n)) (dM : 'M[R]_(m, n)) (x v : V) : (forall i j, is_derive x v (fun t => M t i j) (dM i j)) -> is_derive x v M dM.