Theorem: book.irrational.exponential_series (FormalBook/Chapter_08.lean)

State before:
x : ℝ
⊢ HasSum (fun n => x ^ n / ↑n.factorial) x.exp
Tactic:
sorry
State after:
no goals