Order_of_Conjugate_Element_equals_Order_of_Element
Provedconjugationgroup-theoryorderproofwiki
In a group, the order of x * a * x⁻¹ equals the order of a.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Order_of_Conjugate_Element_equals_Order_of_Element {G : Type _} [Group G] (a x : G) : orderOf (x * a * x⁻¹) = orderOf a := by sorrySource