proposition: Theorem equiv_quotient_abgroup_ump {F : Funext} {G : AbGroup} (N : Subgroup G) (H : Group) : {f : GroupHomomorphism G H & forall (n : G), N n -> f n = mon_unit} <~> (GroupHomomorphism (QuotientAbGroup G N) H).
proof: Proof. exact (equiv_grp_quotient_ump (Build_NormalSubgroup G N _) _). Defined.
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