diff options
| -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. |