Powers_of_Infinite_Order_Element
Provedgroup-theoryinfinite-orderorderproofwiki
Let G be a group and a an element of infinite order. Then for all integers m ≠ n, a^m ≠ a^n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Powers_of_Infinite_Order_Element {G : Type _} [Group G] (a : G) (hinf : orderOf a = 0) (m n : ℤ) (hmn : m ≠ n) : a ^ m ≠ a ^ n := by sorrySource