Inverse_of_Generator_of_Cyclic_Group_is_Generator

Proved

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

cyclic-groupsgeneratorsgroup-theoryproofwiki

Let $\gen g = G$ be a cyclic group. Then $G = \gen {g^{-1} }$ where $g^{-1}$ denotes the inverse of $g$ . Thus, in general, a generator of a cyclic group is not unique.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Inverse_of_Generator_of_Cyclic_Group_is_Generator {G : Type _} [Group G] (g : G) (hg : Subgroup.closure {g} = ⊤) : Subgroup.closure {g⁻¹} = ⊤ := by sorry

Source

https://proofwiki.org/wiki/Inverse_of_Generator_of_Cyclic_Group_is_Generator

View graph