{G : Group@{u}} {A : AbGroup@{u}} (f : GroupHomomorphism G A) : AbGroup := QuotientAbGroup _ (grp_image f).
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.