Self_Inverse_Elements_Commute_iff_Product_is_Self_Inverse
Provedcommutativitygroup-theoryproofwiki
In a group, two self-inverse elements commute if and only if their product is also self-inverse.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Self_Inverse_Elements_Commute_iff_Product_is_Self_Inverse {G : Type _} [Group G] (x y : G) (hx : x * x = 1) (hy : y * y = 1) : x * y = y * x ↔ (x * y) * (x * y) = 1 := by sorrySource