Order_of_Group_Element_equals_Order_of_Inverse
Provedgroup-theoryinverseorderproofwiki
In any group, the order of an element equals the order of its inverse: orderOf(x) = orderOf(x⁻¹).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Order_of_Group_Element_equals_Order_of_Inverse {G : Type _} [Group G] (x : G) : orderOf x = orderOf x⁻¹ := by sorrySource