diff options
| author | affeldt-aist | 2020-11-20 12:41:11 +0900 |
|---|---|---|
| committer | GitHub | 2020-11-20 12:41:11 +0900 |
| commit | 3bb1ccc63170e3e71ef9d5b62758b6fdb1c4371c (patch) | |
| tree | 076b8d8c53eaaf424258388bbd0068970c55b85f /mathcomp/algebra/mxalgebra.v | |
| parent | 676a9266ad77232ab198c86a6a3a3f3f6ba53cc0 (diff) | |
| parent | e565f8d9bebd4fd681c34086d5448dbaebc11976 (diff) | |
Merge pull request #658 from CohenCyril/duplicate_clear
Removing duplicate clears and turning the warning into an error
Diffstat (limited to 'mathcomp/algebra/mxalgebra.v')
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index cc3c6c6..dde8843 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -885,7 +885,7 @@ Lemma eq_genmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :=: B -> <<A>> = <<B>>)%MS. Proof. move=> eqAB; rewrite unlock. -have{eqAB} eqAB: equivmx A (row_full A) =1 equivmx B (row_full B). +have{} eqAB: equivmx A (row_full A) =1 equivmx B (row_full B). by move=> C; rewrite /row_full /equivmx !eqAB. rewrite (eq_choose eqAB) (choose_id _ (genmx_witnessP B)) //. by rewrite -eqAB genmx_witnessP. @@ -1379,7 +1379,7 @@ Let capmx_norm_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : qidmx A = qidmx B -> (A == B)%MS -> capmx_norm A = capmx_norm B. Proof. move=> eqABid /eqmxP eqAB. -have{eqABid eqAB} eqAB: equivmx A (qidmx A) =1 equivmx B (qidmx B). +have{eqABid} eqAB: equivmx A (qidmx A) =1 equivmx B (qidmx B). by move=> C; rewrite /equivmx eqABid !eqAB. rewrite {1}/capmx_norm (eq_choose eqAB). by apply: choose_id; first rewrite -eqAB; apply: capmx_witnessP. |