R : Type ?u.3804
S : Type ?u.3807
M : Type u_1
inst✝ : MonoidWithZero M
k : ℕ
x✝ : k + 1 ≠ 0
⊢ 0 * 0 ^ k = 0
R : Type ?u.3804
S : Type ?u.3807
M : Type u_1
inst✝ : MonoidWithZero M
k : ℕ
x✝ : k + 1 ≠ 0
⊢ 0 ^ (k + 1) = 0
rw [pow_succ]
no goals
R : Type ?u.3804
S : Type ?u.3807
M : Type u_1
inst✝ : MonoidWithZero M
k : ℕ
x✝ : k + 1 ≠ 0
⊢ 0 * 0 ^ k = 0
exact zero_mul _