no goals
x : ℂ
n : ℕ
⊢ x ^ ↑↑n = x ^ ↑n
simp
x : ℂ
n : ℕ
⊢ x ^ ↑-[n+1] = (x ^ (n + 1))⁻¹
x : ℂ
n : ℕ
⊢ x ^ ↑-[n+1] = x ^ -[n+1]
rw [zpow_negSucc]
no goals
x : ℂ
n : ℕ
⊢ x ^ ↑-[n+1] = (x ^ (n + 1))⁻¹
simp only [Int.negSucc_coe, Int.cast_neg, Complex.cpow_neg, inv_eq_one_div, Int.cast_ofNat,
  cpow_nat_cast]