Group_Abelian_iff_Middle_Cancellation_Property
Provedabelian-groupsgroup-theoryproofwiki
Let G be a group. Then G is abelian iff G satisfies the middle cancellation property.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Group_Abelian_iff_Middle_Cancellation_Property {G : Type _} [Group G] : (∀ a b : G, a * b = b * a) ↔ (∀ a b c : G, a * b * c = a * c * b) := by sorrySource