Commutation_Property_in_Group
Provedcommutativitygroup-theoryproofwiki
In a group, x and y commute if and only if x * y * x⁻¹ = y.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Commutation_Property_in_Group {G : Type _} [Group G] (x y : G) : x * y = y * x ↔ x * y * x⁻¹ = y := by sorrySource