case inl
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
h : n = 0
⊢ 0 ^ n = 1

case inr
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else 0
split_ifs with h
no goals
case inl
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
h : n = 0
⊢ 0 ^ n = 1
rw [h, zpow_zero]
no goals
case inr
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0
rw [zero_zpow _ h]