Equivalent_Characterizations_of_Abelian_Group
Provedabelian-groupsproofwiki
Let G be a group. Then G is abelian if and only if for all a, b in G, (ab)⁻¹ = a⁻¹b⁻¹.
Preamble
import Mathlib.Algebra.Group.Basic
Formal statement
theorem Equivalent_Characterizations_of_Abelian_Group {G : Type _} [Group G] : (∀ a b : G, a * b = b * a) ↔ (∀ a b : G, (a * b)⁻¹ = a⁻¹ * b⁻¹) := by sorrySource