no goals
α : Type ?u.67516
β : Type ?u.67519
ι : Type ?u.67522
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ ContinuousAt Inv.inv x ↔ x ≠ 0
simpa [(zero_lt_one' ℤ).not_le] using @continuousAt_zpow _ _ (-1) x