no goals
G : Type u_1
inst✝² : Group G
A : Type ?u.41553
inst✝¹ : AddGroup A
N : Type ?u.41559
inst✝ : Group N
s : Set G
g : G
S : Set G
hS : closure S = ⊤
⊢ center G = ⨅ (g : G) (_ : g ∈ S), centralizer (zpowers g)
rw [← centralizer_top, ← hS, centralizer_closure]