From 1e60610195e93afcfb05bad697573d36a737586f Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Wed, 3 Jul 2024 08:37:34 -0400 Subject: [PATCH] AbGroups/Z: get rid of abgroup_int_mult --- theories/Algebra/AbGroups/Z.v | 7 ------- 1 file changed, 7 deletions(-) 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.