exp_series_hasSum_exp' — Mathlib

English

Variant HasSum for the series with inverse factorials equals exp(x).

Русский

Вариант HasSum для ряда с обратными факториалами даёт exp(x).

LaTeX

$$$\text{HasSum } \left( (n !^{-1}) \cdot x^n \right) = \exp 𝕂 x$$$

Lean4

theorem exp_series_hasSum_exp' (x : 𝔸) : HasSum (fun n => (n !⁻¹ : 𝕂) • x ^ n) (exp 𝕂 x) :=
  expSeries_hasSum_exp_of_mem_ball' x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

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