exp_eq_ofScalarsSum — Mathlib

English

Another formulation: exp 𝕂 equals the scalar-sum representation with coefficients (1/n!).

Русский

Другая формулировка: экспоненциальная карта равна представлению через суммы скаляров с коэффициентами (1/n!).

LaTeX

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

Lean4

/-- The exponential sum as an `ofScalarsSum`. -/
theorem exp_eq_ofScalarsSum : exp 𝕂 = ofScalarsSum (E := 𝔸) fun n ↦ (n !⁻¹ : 𝕂) := by
  rw [exp_eq_tsum, ofScalarsSum_eq_tsum]

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