no goals
G : Type u_1
inst✝² : Group G
A : Type ?u.30840
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers (↑f x)
rw [Subgroup.zpowers_eq_closure, Subgroup.zpowers_eq_closure, f.map_closure, Set.image_singleton]