AbGroups/Z: get rid of abgroup_int_mult

HoTT · Jul 3, 2024 · 1e60610 · 1e60610
1 parent 43e08df
commit 1e60610
Showing 1 changed file with 0 additions and 7 deletions.
diff --git 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.