expSeries_sum_eq — Mathlib

English

The exponential map equals the sum of its exponential series in the standard tsum sense.

Русский

Экспоненциальная карта равна сумме экспоненциальной серии в стандартном смысле суммирования.

LaTeX

$$$\exp 𝕂 = \lambda x. \sum'_{n:\mathbb{N}} \frac{1}{n!} x^{n}$$$

Lean4

theorem expSeries_sum_eq (x : 𝔸) : (expSeries 𝕂 𝔸).sum x = ∑' n : ℕ, (n !⁻¹ : 𝕂) • x ^ n :=
  tsum_congr fun n => expSeries_apply_eq x n

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