Group_equals_Center_iff_Abelian
Provedabelian-groupscenterproofwiki
Let G be a group. Then G is abelian iff Z(G) = G.
Preamble
import Mathlib.GroupTheory.Subgroup.Center
Formal statement
theorem Group_equals_Center_iff_Abelian {G : Type _} [Group G] : (∀ g : G, g ∈ Subgroup.center G) ↔ ∀ a b : G, a * b = b * a := by sorrySource