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 | |
| parent | 9adc523e89022fc6ac77471fb3fe381ad344d060 (diff) | |
Adding [row|col]_[udlr]submx lemmas
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 12 |
2 files changed, 14 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 20809f3..d88a667 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -83,6 +83,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). * `mxOver S` is a subring for square matrices if `S` is. - in `matrix.v` new lemmas about `map_mx`: `map_mx_id`, `map_mx_comp`, `eq_in_map_mx`, `eq_map_mx` and `map_mx_id_in`. +- in `matrix.v`, new lemmas `row_usubmx`, `row_dsubmx`, `col_lsubmx`, + and `col_rsubmx`. ### Changed 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. |