From ec27d03aa60cc87eabb24a832284901e2517faf1 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 25 Aug 2020 00:21:43 +0200
Subject: Adding more map_mx lemmas

---
 CHANGELOG_UNRELEASED.md   |  2 ++
 mathcomp/algebra/matrix.v | 24 ++++++++++++++++++++++++
 2 files changed, 26 insertions(+)

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 *******************)
 (*****************************************************************************)
-- 
cgit v1.2.3