fact: Definition Z1_rec {G : Group@{u}} (g : G) : Z1 $-> G := FreeGroup_rec Unit G (unit_name g).
imports: Basics Types WildCat.Core Truncations.Core AbelianGroup AbHom Centralizer AbProjective Groups.FreeGroup AbGroups.Z Int.Core