no goals
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
⊢ image (fun i => a ^ i) (range (Fintype.card α)) = univ
rw [← orderOf_eq_card_of_forall_mem_zpowers ha, IsCyclic.image_range_orderOf ha]