no goals
x✝ y x : ℂ
⊢ exp (↑0 * x) = exp x ^ 0
rw [Nat.cast_zero, zero_mul, exp_zero, pow_zero]
no goals
x✝ y x : ℂ
n : ℕ
⊢ exp (↑(Nat.succ n) * x) = exp x ^ Nat.succ n
rw [pow_succ', Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]