R : Type ?u.34697
S : Type ?u.34700
M : Type u_1
inst✝ : MonoidWithZero M
a : M
n : ℕ
hn : n ≠ 0
⊢ a = 0 → a ^ n = 0
R : Type ?u.34697
S : Type ?u.34700
M : Type u_1
inst✝ : MonoidWithZero M
a : M
n : ℕ
hn : n ≠ 0
⊢ a ^ n ≠ 0 → a ≠ 0
contrapose!
R : Type ?u.34697
S : Type ?u.34700
M : Type u_1
inst✝ : MonoidWithZero M
n : ℕ
hn : n ≠ 0
⊢ 0 ^ n = 0
R : Type ?u.34697
S : Type ?u.34700
M : Type u_1
inst✝ : MonoidWithZero M
a : M
n : ℕ
hn : n ≠ 0
⊢ a = 0 → a ^ n = 0
rintro rfl
no goals
R : Type ?u.34697
S : Type ?u.34700
M : Type u_1
inst✝ : MonoidWithZero M
n : ℕ
hn : n ≠ 0
⊢ 0 ^ n = 0
exact zero_pow' n hn