{A : AbGroup} (n : Int) : GroupHomomorphism A A. Proof. snrapply Build_GroupHomomorphism. 1: exact (fun a => grp_pow a n). intros a b. apply grp_pow_mul, ab_comm. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.