All_Elements_Self_Inverse_then_Abelian
Provedabelian-groupsproofwiki
If every element of a group is self-inverse, then the group is abelian.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem All_Elements_Self_Inverse_then_Abelian {G : Type _} [Group G] (h : ∀ x : G, x * x = 1) (a b : G) : a * b = b * a := by sorrySource