diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
index 1dcde9e0927..d476119a3f1 100644
--- a/theories/Algebra/AbGroups/Z.v
+++ b/theories/Algebra/AbGroups/Z.v
@@ -22,8 +22,6 @@ Proof.
   - exact int_add_comm.
 Defined.
 
-Local Open Scope mc_scope.
-
 (** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism. *)
 Definition grp_pow_homo {G : Group} (g : G)
   : GroupHomomorphism abgroup_Z G.
@@ -32,8 +30,3 @@ Proof.
   1: exact (grp_pow g).
   intros m n; apply grp_pow_add.
 Defined.
-
-(** The special case for an abelian group, which gives multiplication by an integer. *)
-Definition abgroup_int_mult (A : AbGroup) (a : A)
-  : GroupHomomorphism abgroup_Z A
-  := grp_pow_homo a.