Cyclic_Group_is_Abelian
Provedabeliancyclicgroup-theoryproofwiki
Every cyclic group is abelian.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Cyclic_Group_is_Abelian {G : Type _} [Group G] [IsCyclic G] (a b : G) : a * b = b * a := by sorrySource