From eac1d28204c93f082771dedb90fc5a1edec6e6f8 Mon Sep 17 00:00:00 2001 From: Anton Trunov Date: Tue, 28 May 2019 22:57:38 +0300 Subject: Add eqsP view to destruct not only x == y, but also y == x --- mathcomp/algebra/matrix.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/algebra/matrix.v') diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index d3142d6..91c7747 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 eq_sym; case: eqP => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqsP => // ->. 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 eq_sym; case: eqP => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqsP => // ->. 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 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/matrix.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/algebra/matrix.v') 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 From 42db44ce8df9f24d90c321d57e81e2d5bf83bd48 Mon Sep 17 00:00:00 2001 From: Anton Trunov Date: Wed, 29 May 2019 15:17:39 +0300 Subject: Replace eqVneq with eqPsym Also changed eqsVneq. --- mathcomp/algebra/matrix.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/algebra/matrix.v') diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index ff9d43a..9d6e2be 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: eqPsym => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. 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: eqPsym => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. 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