α : Type u
a : α
inst✝² : Group α
inst✝¹ : Finite α
inst✝ : IsCyclic α
⊢ ∃ x, ∀ (y : α), y ∈ zpowers x
α : Type u
a : α
inst✝² : Group α
inst✝¹ : Finite α
inst✝ : IsCyclic α
⊢ ∃ x, ∀ (y : α), y ∈ Submonoid.powers x
simp_rw [mem_powers_iff_mem_zpowers]
no goals
α : Type u
a : α
inst✝² : Group α
inst✝¹ : Finite α
inst✝ : IsCyclic α
⊢ ∃ x, ∀ (y : α), y ∈ zpowers x
exact IsCyclic.exists_generator