Theorem: ExpTaylorSeriesSummable (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
z : ℂ
⊢ Summable fun k => z ^ k / ↑k.factorial
Tactic:
exact expSeries_div_summable ℂ z
State after:
no goals