expSeries_sum_eq_div — Mathlib

English

The sum of the expSeries over n equals the infinite series sum of x^n / n!, i.e., the exponential function is the sum of these terms.

Русский

Сумма expSeries по n равна сумме по n: x^n / n!, то есть экспонента есть сумма этих членов.

LaTeX

$$$(\\expSeries 𝕂 𝔸).sum x = \\sum_{n=0}^{\\infty} \\dfrac{x^{n}}{n!}$$$

Lean4

theorem expSeries_sum_eq_div (x : 𝔸) : (expSeries 𝕂 𝔸).sum x = ∑' n : ℕ, x ^ n / n ! :=
  tsum_congr (expSeries_apply_eq_div x)

Похожие утверждения