no goals
α : Type ?u.290494
G : Type ?u.290497
M : Type ?u.290500
R : Type u_1
A : Type ?u.290506
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : Semiring R
s : AddSubmonoid R
n : ℕ
⊢ s ^ n = closure (↑s ^ n)
rw [← closure_pow, closure_eq]