Quotient_of_Group_by_Center_Cyclic_implies_Abelian
Provedabeliancentercyclicgroup-theoryproofwiki
If the quotient of a group G by its center Z(G) is cyclic, then G is abelian (and hence G = Z(G)).
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.GroupTheory.SpecificGroups.Cyclic
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.GroupTheory.SpecificGroups.Cyclic
theorem Quotient_of_Group_by_Center_Cyclic_implies_Abelian {G : Type _} [Group G] (h : IsCyclic (G ⧸ Subgroup.center G)) : ∀ a b : G, a * b = b * a := by sorrySource