Group_Element_is_Self_Inverse_iff_Order_2
Provedgroup-theoryinverseorderproofwiki
An element x of a group (with x not the identity) is self-inverse if and only if x has order 2.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Group_Element_is_Self_Inverse_iff_Order_2 {G : Type _} [Group G] (x : G) (hx : x ≠ 1) : x = x⁻¹ ↔ orderOf x = 2 := by sorrySource