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.