exp_eq_tsum — Mathlib

English

The exponential map equals the sum with scalar coefficients given by 1/n!: exp 𝕂 = ofScalarsSum (E := 𝔸) (n ↦ (n!)^{-1}).

Русский

Экспоненциальная карта равна сумме со скалярами 1/n!: exp 𝕂 = ofScalarsSum (E := 𝔸) (n ↦ (n!)^{-1}).

LaTeX

$$$\exp 𝕂 = \mathrm{ofScalarsSum}(E := 𝔸)\; (n \mapsto (n!)^{-1})$$$

Lean4

theorem exp_eq_tsum : exp 𝕂 = fun x : 𝔸 => ∑' n : ℕ, (n !⁻¹ : 𝕂) • x ^ n :=
  funext expSeries_sum_eq

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