Theorems · Theorem · sequences and series

Real.summable_pow_div_factorial

∀ (x : ℝ), Summable fun n => x ^ n / ↑n.factorial

The series ∑' n, x ^ n / n! is summable of any x : ℝ. See also expSeries_div_summable for a version that also works in ℂ, and NormedSpace.expSeries_summable' for a version that works in any normed algebra over ℝ or ℂ.

Defined in

Mathlib.Analysis.SpecificLimits.Normed

Cited by

1 results in Mathlib

Foundations

Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound