Non_Trivial_Group_has_Non_Trivial_Cyclic_Subgroup
Provedcyclicgroup-theoryproofwikisubgroup
Let G be a group and g a non-identity element. Then the cyclic subgroup generated by g is non-trivial.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Non_Trivial_Group_has_Non_Trivial_Cyclic_Subgroup {G : Type _} [Group G] (g : G) (hg : g ≠ 1) : Subgroup.zpowers g ≠ ⊥ := by sorrySource