{G : AbGroup} (N : Subgroup G) (H : AbGroup) (f : GroupHomomorphism G H) (h : forall n : G, N n -> f n = mon_unit) : GroupHomomorphism (QuotientAbGroup G N) H := grp_quotient_rec G (Build_NormalSubgroup G N _) f h.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.