From 5d90649f226e80256ad903db9b8a0c21042f5a0a Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 3 Sep 2020 12:59:09 +0200
Subject: Lemma mul_rvP

---
 mathcomp/algebra/matrix.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index a7920ed..100eed7 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -1678,6 +1678,9 @@ apply/rowP=> j; rewrite !mxE (bigD1_ord i) //= mxE !eqxx mul1r.
 by rewrite big1 ?addr0 // => i'; rewrite mxE /= lift_eqF mul0r.
 Qed.
 
+Lemma mul_rVP m n A B :((@mulmx 1 m n)^~ A =1 mulmx^~ B) <-> (A = B).
+Proof. by split=> [eqAB|->//]; apply/row_matrixP => i; rewrite !rowE eqAB. Qed.
+
 Lemma row_mul m n p (i : 'I_m) A (B : 'M_(n, p)) :
   row i (A *m B) = row i A *m B.
 Proof. by rewrite !rowE mulmxA. Qed.
-- 
cgit v1.2.3