expSeries_eq_ofScalars — Mathlib

English

A variant form of expSeries equality to a scalar-coefficient representation: expSeries 𝕂 𝔸 equals ofScalars 𝔸 with coefficients inv(n!).

Русский

Вариант выражения expSeries через скаляры: expSeries 𝕂 𝔸 равен ofScalars 𝔸 со коэффициентами 1/n!.

LaTeX

$$$\expSeries 𝕂 𝔸 = \mathrm{ofScalars}_{𝔸} (n \mapsto (n!)^{-1})$$$

Lean4

/-- The exponential series as an `ofScalars` series. -/
theorem expSeries_eq_ofScalars : expSeries 𝕂 𝔸 = ofScalars 𝔸 fun n ↦ (n !⁻¹ : 𝕂) := by
  simp_rw [FormalMultilinearSeries.ext_iff, expSeries, ofScalars, implies_true]

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