β : Type ?u.274493
A : Type ?u.274496
G : Type ?u.274499
M : Type u_1
R : Type ?u.274505
inst✝¹ : LinearOrderedCommMonoidWithZero M
inst✝ : NoZeroDivisors M
a : M
n : ℕ
hn : 0 < n
⊢ a ^ n ≠ 0 ↔ a ≠ 0
β : Type ?u.274493
A : Type ?u.274496
G : Type ?u.274499
M : Type u_1
R : Type ?u.274505
inst✝¹ : LinearOrderedCommMonoidWithZero M
inst✝ : NoZeroDivisors M
a : M
n : ℕ
hn : 0 < n
⊢ 0 < a ^ n ↔ 0 < a
simp_rw [zero_lt_iff]
no goals
β : Type ?u.274493
A : Type ?u.274496
G : Type ?u.274499
M : Type u_1
R : Type ?u.274505
inst✝¹ : LinearOrderedCommMonoidWithZero M
inst✝ : NoZeroDivisors M
a : M
n : ℕ
hn : 0 < n
⊢ a ^ n ≠ 0 ↔ a ≠ 0
rw [pow_ne_zero_iff hn]