From 8b98bcedc4523e07e4fdc118159cf171366e952d Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Mon, 9 Nov 2020 01:06:18 +0100
Subject: `comm(Cmx|_mxC)` -> `comm(_scalar_mx|_mx_scalar)`

---
 mathcomp/algebra/mxalgebra.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/algebra/mxalgebra.v')

diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index e65bc3c..7aa89b8 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -2291,7 +2291,7 @@ Lemma comm_mx_stable_eigenspace (f g : 'M[F]_n) a :
   comm_mx f g -> stablemx (eigenspace f a) g.
 Proof.
 move=> cfg; rewrite comm_mx_stable_ker//.
-by apply/comm_mx_sym/comm_mxB => //; apply:comm_mxC.
+by apply/comm_mx_sym/comm_mxB => //; apply:comm_mx_scalar.
 Qed.
 
 End Commutation.
-- 
cgit v1.2.3