fact: Definition Z1_to_Z `{Funext} : ab_Z1 $-> abgroup_Z := Z1_rec (G:=abgroup_Z) 1%int.
imports: Basics Types WildCat.Core Truncations.Core AbelianGroup AbHom Centralizer AbProjective Groups.FreeGroup AbGroups.Z Int.Core