From 81fec2fc28635ff88e1ee313bf5d4cc678b00689 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Mon, 1 Jan 2024 22:28:38 +0900
Subject: [PATCH] rm dup lemmas (#1129)

---
 CHANGELOG_UNRELEASED.md | 3 +++
 theories/forms.v        | 7 -------
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 3c9ab8514..fc967ae88 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -90,6 +90,9 @@
 
 ### Removed
 
+- in `forms.v`:
+  + lemmas `eq_map_mx`, `map_mx_id`
+
 ### Infrastructure
 
 ### Misc
diff --git a/theories/forms.v b/theories/forms.v
index 881a498b6..04f1680f3 100644
--- a/theories/forms.v
+++ b/theories/forms.v
@@ -39,13 +39,6 @@ Structure revop X Y Z (f : Y -> X -> Z) := RevOp {
   _ : forall x, f x =1 fun_of_revop^~ x
 }.
 
-Lemma eq_map_mx (R S : ringType) m n (M : 'M[R]_(m,n))
-      (g f : R -> S) : f =1 g -> M ^ f = M ^ g.
-Proof. by move=> eq_fg; apply/matrixP=> i j; rewrite !mxE. Qed.
-
-Lemma map_mx_id (R : ringType) m n (M : 'M[R]_(m,n)) : M ^ id = M.
-Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.
-
 Lemma eq_map_mx_id (R : ringType) m n (M : 'M[R]_(m,n)) (f : R -> R) :
   f =1 id -> M ^ f = M.
 Proof. by move=> /eq_map_mx->; rewrite map_mx_id. Qed.