diff options
| author | Anton Trunov | 2019-05-28 22:57:38 +0300 |
|---|---|---|
| committer | Anton Trunov | 2019-05-28 23:56:19 +0300 |
| commit | eac1d28204c93f082771dedb90fc5a1edec6e6f8 (patch) | |
| tree | 1d3709a7e13e1db2508253213ee690af1e222d2c /mathcomp/algebra | |
| parent | 748d716efb2f2f75946c8386e441ce1789806a39 (diff) | |
Add eqsP view to destruct not only x == y, but also y == x
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 48e9de8..77f8781 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 eq_sym; case: eqP => // ->. + by apply/matrixP=> i1 j1; rewrite !mxE; case: eqsP => // ->. 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 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. |