fact: Definition projection_split_iso1 {B A : AbGroup} (E : AbSES B A) {s : GroupHomomorphism B E} (h : (projection _) $o s == idmap) : GroupIsomorphism E (ab_biprod (@ab_kernel E B (projection _)) B).
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse