Series_of_Power_over_Factorial_Converges

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwikiseries

The series $\displaystyle \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$ converges for all real values of $x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Series_of_Power_over_Factorial_Converges (x : ℝ) : Summable (fun n : ℕ => x ^ n / ↑(Nat.factorial n)) := by sorry

Source