Generators_of_Infinite_Cyclic_Group

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

cyclic-groupsgeneratorsgroup-theoryinfinite-groupsproofwiki

Let $\gen g = G$ be an infinite cyclic group. Then the only other generator of $G$ is $g^{-1}$ . Thus an infinite cyclic group has exactly $2$ generators.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Generators_of_Infinite_Cyclic_Group {G : Type _} [Group G] [Infinite G] (g : G) (hg : Subgroup.closure {g} = ⊤) (h : G) (hh : Subgroup.closure {h} = ⊤) : h = g ∨ h = g⁻¹ := by sorry

Source

https://proofwiki.org/wiki/Generators_of_Infinite_Cyclic_Group

View graph