expSeries_apply_eq_div' — Mathlib

English

Same as above for the primed version: the n-th term equals x^n / n!, interpreted in the primed formulation.

Русский

Та же структура для производной версии: n-ый член равен x^n / n! в примированной формулировке.

LaTeX

$$$(\\expSeries 𝕂 𝔸 n) (\\underbrace{x, \\dots, x}_{n\\text{ times}}) = \\dfrac{x^{n}}{n!}$$$

Lean4

theorem expSeries_apply_eq_div' (x : 𝔸) : (fun n => expSeries 𝕂 𝔸 n fun _ => x) = fun n => x ^ n / n ! :=
  funext (expSeries_apply_eq_div x)

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