no goals
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
k : ℕ
x : 𝕜
⊢ (deriv^[k]) Inv.inv x = (∏ i in Finset.range k, (-1 - ↑i)) * x ^ (-1 - ↑k)
simpa only [zpow_neg_one, Int.cast_neg, Int.cast_one] using iter_deriv_zpow (-1) x k