fact: Definition ab_pushout_inr {A B C : AbGroup} {f : A $-> B} {g : A $-> C} : C $-> ab_pushout f g := grp_quotient_map $o grp_prod_inr.
imports: Basics Types Truncations.Core Modalities.ReflectiveSubuniverse WildCat.Core HSet Algebra.Groups.Image Algebra.Groups.QuotientGroup AbGroups.AbelianGroup AbGroups.Biproduct