G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
x : G₀
h : x ≠ 0
⊢ (x ^ n)⁻¹ * x ^ n = 1
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
x : G₀
h : x ≠ 0
⊢ x ^ (-n) * x ^ n = 1
rw [zpow_neg]
no goals
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
x : G₀
h : x ≠ 0
⊢ (x ^ n)⁻¹ * x ^ n = 1
exact inv_mul_cancel (zpow_ne_zero n h)