M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.80130
inst✝¹ : CommMonoid N
P : Type ?u.80136
inst✝ : CommMonoid P
n : ℕ
a : M
b : { x // x ∈ S }
⊢ Monoid.npow n (mk a b) = mk (a ^ n) (b ^ n)
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.80130
inst✝¹ : CommMonoid N
P : Type ?u.80136
inst✝ : CommMonoid P
n : ℕ
a : M
b : { x // x ∈ S }
⊢ Localization.npow S n (mk a b) = mk (a ^ n) (b ^ n)
rw [Localization.npow]
no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.80130
inst✝¹ : CommMonoid N
P : Type ?u.80136
inst✝ : CommMonoid P
n : ℕ
a : M
b : { x // x ∈ S }
⊢ Monoid.npow n (mk a b) = mk (a ^ n) (b ^ n)
rfl