rm dup lemmas (math-comp#1129)

affeldt-aist · Jan 9, 2024 · cb20f23 · cb20f23
1 parent d2c1665
commit cb20f23
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 7 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -95,6 +95,9 @@
 
 ### Removed
 
+- in `forms.v`:
+  + lemmas `eq_map_mx`, `map_mx_id`
+
 ### Infrastructure
 
 ### Misc
diff --git a/theories/forms.v b/theories/forms.v
@@ -40,13 +40,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.