From c7c344f2f08f3910c884d9c3bb1bd5cfe3c2a1d7 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Wed, 29 May 2019 12:38:48 +0300
Subject: Rename eqsP to eqPsym as suggested by @CohenCyril

---
 mathcomp/algebra/intdiv.v | 2 +-
 mathcomp/algebra/matrix.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/algebra')

diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 77f8781..edd2620 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -969,7 +969,7 @@ without loss{IHa} /forallP/(_ (_, _))/= a_dvM: / [forall k, a %| M k.1 k.2]%Z.
     by exists i; rewrite mxE.
   exists R^T; last exists L^T; rewrite ?unitmx_tr //; exists d => //.
   rewrite -[M]trmxK dM !trmx_mul mulmxA; congr (_ *m _ *m _).
-  by apply/matrixP=> i1 j1; rewrite !mxE; case: eqsP => // ->.
+  by apply/matrixP=> i1 j1; rewrite !mxE; case: eqPsym => // ->.
 without loss{nz_a a_dvM} a1: M a Da / a = 1.
   pose M1 := map_mx (divz^~ a) M; case/(_ M1 1)=> // [k|L uL [R uR [d dvD dM]]].
     by rewrite !mxE Da divzz nz_a.
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 91c7747..ff9d43a 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -1392,7 +1392,7 @@ Definition diag_mx n (d : 'rV[R]_n) :=
   \matrix[diag_mx_key]_(i, j) (d 0 i *+ (i == j)).
 
 Lemma tr_diag_mx n (d : 'rV_n) : (diag_mx d)^T = diag_mx d.
-Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqsP => // ->. Qed.
+Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqPsym => // ->. Qed.
 
 Lemma diag_mx_is_linear n : linear (@diag_mx n).
 Proof.
@@ -1744,7 +1744,7 @@ by rewrite eqn_leq andbC leqNgt lshift_subproof.
 Qed.
 
 Lemma tr_pid_mx m n r : (pid_mx r)^T = pid_mx r :> 'M_(n, m).
-Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqsP => // ->. Qed.
+Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqPsym => // ->. Qed.
 
 Lemma pid_mx_minv m n r : pid_mx (minn m r) = pid_mx r :> 'M_(m, n).
 Proof. by apply/matrixP=> i j; rewrite !mxE leq_min ltn_ord. Qed.
-- 
cgit v1.2.3