theorem CyclicGroups.cyclic_subgroup_structure {G : Type u_1} [Group G] (g : G) : (orderOf g = 0 ∧ Function.Injective fun (n : ℤ) => g ^ n) ∨ 0 < orderOf g ∧ Nat.card ↥(Subgroup.zpowers g) = orderOf g