case a
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ ↑n = 0
rw [zpow_ofNat, zero_pow']
no goals
case a
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0
simpa using h
no goals
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℕ
x✝ : -[n+1] ≠ 0
⊢ 0 ^ -[n+1] = 0
simp