Theorem: cexp_eq_tsum (ExponentialRamsey/Prereq/Mathlib/Analysis/SpecialFunctions/ExplicitStirling.lean)

State before:
x : ℂ
⊢ Complex.exp x = ∑' (i : ℕ), x ^ i / ↑i !
Tactic:
rw [Complex.exp_eq_exp_ℂ, exp_eq_tsum_div]
State after:
no goals