expSeries_apply_eq' — Mathlib

English

The exponential map is given by summing its exponential series termwise: exp 𝕂 x = sum_{n≥0} (1/n!) x^n.

Русский

Экспоненциальная карта задаётся суммой экспоненциальной серии по каждому рангу: exp 𝕂 x = сумма_{n≥0} (1/n!) x^n.

LaTeX

$$$\exp 𝕂 = \lambda x. \sum_{n=0}^{\infty} (n!)^{-1} x^{n}$$$

Lean4

theorem expSeries_apply_eq' (x : 𝔸) : (fun n => expSeries 𝕂 𝔸 n fun _ => x) = fun n => (n !⁻¹ : 𝕂) • x ^ n :=
  funext (expSeries_apply_eq x)

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