Theorem: ExpTsumForm (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
z : ℂ
⊢ cexp z = ∑' (k : ℕ), z ^ k / ↑k.factorial
Tactic:
rw [exp_eq_exp_ℂ, exp_eq_tsum_div]
State after:
no goals