Group_of_Order_less_than_6_is_Abelian
Provedabelianfinite-groupgroup-theoryproofwiki
All groups with fewer than 6 elements are abelian.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Group_of_Order_less_than_6_is_Abelian {G : Type _} [Group G] [Fintype G] (h : Fintype.card G < 6) (a b : G) : a * b = b * a := by sorrySource