diff options
| author | Cyril Cohen | 2020-08-25 00:16:01 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-07 16:45:11 +0200 |
| commit | c2721f5f10d5443d5a10d641a8474f00fc3d07a2 (patch) | |
| tree | 41fbb271e1fe6570dc70e80c35425503658079ec /mathcomp | |
| parent | 9adc523e89022fc6ac77471fb3fe381ad344d060 (diff) | |
Adding [row|col]_[udlr]submx lemmas
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 1730b0b..a7920ed 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -607,6 +607,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. |