Equal_Powers_of_Finite_Order_Element
Provedgroup-theoryorderproofwiki
For a group element g of finite order k, g^r = g^s if and only if k divides (r - s).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Equal_Powers_of_Finite_Order_Element {G : Type _} [Group G] (g : G) (k : ℕ) (hk : orderOf g = k) (hk0 : 0 < k) (r s : ℤ) : g ^ r = g ^ s ↔ (k : ℤ) ∣ (r - s) := by sorrySource