Merge pull request #636 from CohenCyril/fix_comm_mxC

`comm(Cmx|_mxC)` -> `comm(_scalar_mx|_mx_scalar)`

3 files changed, 11 insertions, 10 deletions

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index f7d7730..77d2e4f 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -2889,11 +2889,11 @@ Qed.
 Lemma mul_mx_scalar m n a (A : 'M[R]_(m, n)) : A *m a%:M = a *: A.
 Proof. by rewrite scalar_mxC mul_scalar_mx. Qed.
 
-Lemma comm_mxC n a (A : 'M[R]_n) : comm_mx A a%:M.
+Lemma comm_mx_scalar n a (A : 'M[R]_n) : comm_mx A a%:M.
 Proof. by rewrite /comm_mx mul_mx_scalar mul_scalar_mx. Qed.
 
-Lemma commCmx n a (A : 'M[R]_n) : comm_mx a%:M A.
-Proof. exact/comm_mx_sym/comm_mxC. Qed.
+Lemma comm_scalar_mx n a (A : 'M[R]_n) : comm_mx a%:M A.
+Proof. exact/comm_mx_sym/comm_mx_scalar. Qed.
 
 Lemma mxtrace_mulC m n (A : 'M[R]_(m, n)) B :
    \tr (A *m B) = \tr (B *m A).
@@ -3140,16 +3140,16 @@ End ComMatrix.
 
 Arguments lin_mul_row {R m n} u.
 Arguments lin_mulmx {R m n p} A.
-Arguments comm_mxC {R n}.
-Arguments commCmx {R n}.
+Arguments comm_mx_scalar {R n}.
+Arguments comm_scalar_mx {R n}.
 Arguments diag_mx_comm {R n}.
 
 Canonical matrix_finAlgType (R : finComRingType) n' :=
   [finAlgType R of 'M[R]_n'.+1].
 
-Hint Resolve comm_mxC commCmx : core.
+Hint Resolve comm_mx_scalar comm_scalar_mx : core.
 
-Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mxC)
+Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mx_scalar)
   (at level 10, only parsing) : fun_scope.
 Notation scalar_mx_comm := (@scalar_mx_comm _ _) (only parsing).
 
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.
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index c7f8fb1..19a23e6 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -274,7 +274,7 @@ Section OneMatrix.
 
 Variable A : 'M[R]_n.
 
-Definition horner_mx := horner_morph (comm_mxC^~ A).
+Definition horner_mx := horner_morph (comm_mx_scalar^~ A).
 Canonical horner_mx_additive := [additive of horner_mx].
 Canonical horner_mx_rmorphism := [rmorphism of horner_mx].
 
@@ -317,7 +317,8 @@ Qed.
 
 Lemma comm_mx_horner A B p : comm_mx A B -> comm_mx A (horner_mx B p).
 Proof.
-by move=> fg; apply: commr_horner => // i; rewrite coef_map; apply/commCmx.
+move=> fg; apply: commr_horner => // i.
+by rewrite coef_map; apply/comm_scalar_mx.
 Qed.
 
 Lemma comm_horner_mx A B p : comm_mx A B -> comm_mx (horner_mx A p) B.