diff options
| author | Anton Trunov | 2019-05-29 15:17:39 +0300 |
|---|---|---|
| committer | Anton Trunov | 2019-05-29 15:17:39 +0300 |
| commit | 42db44ce8df9f24d90c321d57e81e2d5bf83bd48 (patch) | |
| tree | c928479b8231901da1cfb4efece42ebe2d419da7 /mathcomp/algebra/intdiv.v | |
| parent | 1aa27b589c437b88cc6fb556edfceac42da449ea (diff) | |
Replace eqVneq with eqPsym
Also changed eqsVneq.
Diffstat (limited to 'mathcomp/algebra/intdiv.v')
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index edd2620..0a5bfde 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: eqPsym => // ->. + by apply/matrixP=> i1 j1; rewrite !mxE; case: eqVneq => // ->. 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. |