diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 22f5e89..02097a4 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -609,6 +609,18 @@ Proof. by split_mxE. Qed. Lemma col_mx_const a : col_mx (const_mx a) (const_mx a) = const_mx a. Proof. by split_mxE. Qed. +Lemma row_usubmx A i : row i (usubmx A) = row (lshift m2 i) A. +Proof. by apply/rowP=> j; rewrite !mxE; congr (A _ _); apply/val_inj. Qed. + +Lemma row_dsubmx A i : row i (dsubmx A) = row (rshift m1 i) A. +Proof. by apply/rowP=> j; rewrite !mxE; congr (A _ _); apply/val_inj. Qed. + +Lemma col_lsubmx A i : col i (lsubmx A) = col (lshift n2 i) A. +Proof. by apply/colP=> j; rewrite !mxE; congr (A _ _); apply/val_inj. Qed. + +Lemma col_rsubmx A i : col i (rsubmx A) = col (rshift n1 i) A. +Proof. by apply/colP=> j; rewrite !mxE; congr (A _ _); apply/val_inj. Qed. + End CutPaste. Lemma trmx_lsub m n1 n2 (A : 'M_(m, n1 + n2)) : (lsubmx A)^T = usubmx A^T. @@ -1874,6 +1886,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. |