Central square commutativity
Abstract
A central square-return word forces the two generators to commute.
Let G be a group and let u,v be elements of G. If the element v inverse times u squared commutes with every element of G, then u and v commute. The proof applies centrality to u, cancels the common right factor u squared, and multiplies the resulting equality by v on the left and right.
Theorem 1.1 (Central square-return commutativity).
Lean statement: D5/S3/Geometry/Hyperideal/CentralSquareCommutativity.central_v_inv_sq_implies_commute
Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/CentralSquareCommutativity.central_v_inv_sq_implies_commute (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every group G and u,v in G, if v inverse times u squared is central, then u times v equals v times u.