n : ℕ
A : Type ?u.324794
R : Type ?u.324797
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_1
inst✝ : Group α
a : α
h : 0 < Nat.card { x // x ∈ zpowers a }
⊢ Finite { x // x ∈ zpowers a }
n : ℕ
A : Type ?u.324794
R : Type ?u.324797
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_1
inst✝ : Group α
a : α
h : IsOfFinOrder a
⊢ Finite { x // x ∈ zpowers a }
rw [← orderOf_pos_iff, order_eq_card_zpowers'] at h
no goals
n : ℕ
A : Type ?u.324794
R : Type ?u.324797
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_1
inst✝ : Group α
a : α
h : 0 < Nat.card { x // x ∈ zpowers a }
⊢ Finite { x // x ∈ zpowers a }
exact Nat.finite_of_card_ne_zero h.ne.symm