Boolean_Group_is_Abelian
Provedabelianboolean-groupgroup-theoryproofwiki
Let G be a Boolean group (every element is its own inverse, i.e., x^2 = 1 for all x). Then G is abelian.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Boolean_Group_is_Abelian {G : Type _} [Group G] (h : ∀ x : G, x * x = 1) (a b : G) : a * b = b * a := by sorrySource