fact: Definition quotient_abgroup_rec {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.
imports: Basics Types Classes.interfaces.canonical_names (Zero, zero) Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative) Algebra.Groups.Group Algebra.Groups.Subgroup Algebra.Groups.QuotientGroup WildCat