{G : Group} (g : G) : GroupHomomorphism abgroup_Z G. Proof. snrapply Build_GroupHomomorphism. 1: exact (grp_pow g). intros m n; apply grp_pow_add. Defined.
Require Import Basics. Require Import Spaces.Pos.Core Spaces.Int. Require Import Algebra.AbGroups.AbelianGroup.