Mapping_to_Square_is_Endomorphism_iff_Abelian
Provedabelian-groupsendomorphismsgroup-theoryproofwiki
The squaring map x ↦ x*x is an endomorphism of a group G if and only if G is abelian.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Mapping_to_Square_is_Endomorphism_iff_Abelian {G : Type _} [Group G] : (∀ a b : G, a * b * (a * b) = a * a * (b * b)) ↔ (∀ a b : G, a * b = b * a) := by sorrySource