R : Type ?u.22317
S : Type ?u.22320
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
a : M
n : ℕ
hn : 0 < n
⊢ a = 0 → a ^ n = 0
R : Type ?u.22317
S : Type ?u.22320
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
a : M
n : ℕ
hn : 0 < n
⊢ a ^ n = 0 ↔ a = 0
refine' ⟨pow_eq_zero, _⟩
R : Type ?u.22317
S : Type ?u.22320
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
n : ℕ
hn : 0 < n
⊢ 0 ^ n = 0
R : Type ?u.22317
S : Type ?u.22320
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
a : M
n : ℕ
hn : 0 < n
⊢ a = 0 → a ^ n = 0
rintro rfl
no goals
R : Type ?u.22317
S : Type ?u.22320
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
n : ℕ
hn : 0 < n
⊢ 0 ^ n = 0
exact zero_pow hn