diff options
| author | Cyril Cohen | 2019-11-06 15:54:03 +0100 |
|---|---|---|
| committer | GitHub | 2019-11-06 15:54:03 +0100 |
| commit | 9a8b8292371526978b9e34804daf114658fe4b7a (patch) | |
| tree | af3b6de4ec0b11f970d699943373af6894fe7115 /mathcomp/algebra/mxalgebra.v | |
| parent | fcffe720b5a66bb6c0d9b6179dbef2b7af8805b6 (diff) | |
| parent | ad84fa64677463ab27a10bcd4d0081fd06693945 (diff) | |
Merge pull request #408 from chdoc/existsPn
add existsPn/forallPn lemmas
Diffstat (limited to 'mathcomp/algebra/mxalgebra.v')
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 8d6c03b..a39aba1 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -609,7 +609,7 @@ Arguments rV_subP {m1 m2 n A B}. Lemma row_subPn m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (exists i, ~~ (row i A <= B)%MS) (~~ (A <= B)%MS). -Proof. by rewrite (sameP row_subP forallP) negb_forall; apply: existsP. Qed. +Proof. by rewrite (sameP row_subP forallP); apply: forallPn. Qed. Lemma sub_rVP n (u v : 'rV_n) : reflect (exists a, u = a *: v) (u <= v)%MS. Proof. |