no goals
R : Type ?u.52055
S : Type ?u.52058
M : Type u_1
inst✝ : MonoidWithZero M
r : M
⊢ inverse r ^ 0 = inverse (r ^ 0)
rw [pow_zero, pow_zero, Ring.inverse_one]
no goals
R : Type ?u.52055
S : Type ?u.52058
M : Type u_1
inst✝ : MonoidWithZero M
r : M
n : ℕ
⊢ inverse r ^ (n + 1) = inverse (r ^ (n + 1))
rw [pow_succ, pow_succ', Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
  Ring.inverse_pow r n]