no goals
G : Type u_1
inst✝² : Group G
A : Type ?u.41951
inst✝¹ : AddGroup A
N : Type ?u.41957
inst✝ : Group N
s : Set G
g : G
S : Set G
hS : closure S = ⊤
⊢ center G = ⨅ (g : ↑S), centralizer (zpowers ↑g)
rw [center_eq_iInf S hS, ← iInf_subtype'']