G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m✝ : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : (fun n => x ^ n) n = (fun n => x ^ n) m
⊢ n = m
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
⊢ (Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x
refine' ⟨fun h => not_isOfFinOrder_of_injective_pow h, fun h n m hnm => _⟩
no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m✝ : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : (fun n => x ^ n) n = (fun n => x ^ n) m
⊢ n = m
rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, modEq_zero_iff] at hnm