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

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