no goals
α : Type ?u.264941
G : Type ?u.264944
M : Type ?u.264947
R : Type u_1
A : Type ?u.264953
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : Semiring R
s : Set R
⊢ closure s ^ 0 = closure (s ^ 0)
rw [pow_zero, pow_zero, one_eq_closure_one_set]
no goals
α : Type ?u.264941
G : Type ?u.264944
M : Type ?u.264947
R : Type u_1
A : Type ?u.264953
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : Semiring R
s : Set R
n : ℕ
⊢ closure s ^ (n + 1) = closure (s ^ (n + 1))
rw [pow_succ, pow_succ, closure_pow s n, closure_mul_closure]