fact: Definition cyclic@{u v | u < v} `{Funext} (n : nat) : AbGroup@{u} := ab_cokernel@{u v} (Z1_mul_nat n).
imports: Basics Types WildCat.Core Truncations.Core AbelianGroup AbHom Centralizer AbProjective Groups.FreeGroup AbGroups.Z Int.Core