G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ a ^ a✝ ≠ 0
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ a ^ ↑a✝ ≠ 0
rw [zpow_ofNat]
no goals
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ a ^ a✝ ≠ 0
exact pow_ne_zero _ ha
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ (a ^ (a✝ + 1))⁻¹ ≠ 0
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ a ^ -[a✝+1] ≠ 0
rw [zpow_negSucc]
no goals
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ (a ^ (a✝ + 1))⁻¹ ≠ 0
exact inv_ne_zero (pow_ne_zero _ ha)