Power_over_Factorial

Proved

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

limits-of-sequencesproofwiki

Let $x \in \R: x > 0$ be a positive real number. Let $\sequence {x_n}$ be the sequence in $\R$ defined as $x_n = \dfrac {x^n} {n!}$ . Then $\sequence {x_n}$ converges to zero.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Power_over_Factorial (x : ℝ) (hx : x > 0) : Filter.Tendsto (fun n : ℕ => x ^ n / ↑(Nat.factorial n)) Filter.atTop (nhds 0) := by sorry

Source

https://proofwiki.org/wiki/Power_over_Factorial

View graph