diff options
| author | Yves Bertot | 2020-09-07 09:52:45 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-07 09:52:45 +0200 |
| commit | 0d8d89239a0fbd5f5c6856e018054e5cc1dfe404 (patch) | |
| tree | 3603d300a228d35da92a54574de612e08f0ea12e | |
| parent | 03dd7f46126c5125c7d166bfbcbb8e4b33b1906c (diff) | |
| parent | ec27d03aa60cc87eabb24a832284901e2517faf1 (diff) | |
Merge pull request #568 from CohenCyril/map_mx
Support for `map_mx`
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 24 |
2 files changed, 26 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index aa6b37b..20809f3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -81,6 +81,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). * `mxOver S` is a sub Z-module if `S` is. * `mxOver S` is a semiring for square matrices if `S` is. * `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`. ### Changed diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index a0ac28f..1730b0b 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1033,6 +1033,30 @@ End MapMatrix. Arguments map_mx {aT rT} f {m n} A. +Section MultipleMapMatrix. +Local Notation "M ^ phi" := (map_mx phi M). + +Lemma map_mx_id (R : Type) m n (M : 'M[R]_(m,n)) : M ^ id = M. +Proof. by apply/matrixP => i j; rewrite !mxE. Qed. + +Lemma map_mx_comp (R S T : Type) m n (M : 'M[R]_(m,n)) + (f : R -> S) (g : S -> T) : M ^ (g \o f) = (M ^ f) ^ g. +Proof. by apply/matrixP => i j; rewrite !mxE. Qed. + +Lemma eq_in_map_mx (R S : Type) m n (M : 'M[R]_(m,n)) (g f : R -> S) : + (forall i j, f (M i j) = g (M i j)) <-> M ^ f = M ^ g. +Proof. by rewrite -matrixP; split => fg i j; have := fg i j; rewrite !mxE. Qed. + +Lemma eq_map_mx (R S : Type) m n (M : 'M[R]_(m,n)) (g f : R -> S) : + f =1 g -> M ^ f = M ^ g. +Proof. by move=> eq_fg; apply/eq_in_map_mx. Qed. + +Lemma map_mx_id_in (R : Type) m n (M : 'M[R]_(m,n)) (f : R -> R) : + (forall i j, f (M i j) = M i j) -> M ^ f = M. +Proof. by rewrite -[RHS]map_mx_id -eq_in_map_mx. Qed. + +End MultipleMapMatrix. + (*****************************************************************************) (********************* Matrix Zmodule (additive) structure *******************) (*****************************************************************************) |