no goals
x : ℂ
⊢ x ^ ↑0 = x ^ 0
simp
no goals
x : ℂ
n : ℕ
hx : x = 0
⊢ x ^ ↑(n + 1) = x ^ (n + 1)
simp only [hx, pow_succ, Complex.zero_cpow (Nat.cast_ne_zero.2 (Nat.succ_ne_zero _)),
  MulZeroClass.zero_mul]
no goals
x : ℂ
n : ℕ
hx : ¬x = 0
⊢ x ^ ↑(n + 1) = x ^ (n + 1)
simp [cpow_add, hx, pow_add, cpow_nat_cast x n]