expSeries_apply_eq — Mathlib

English

A reformulation: the function n ↦ expSeries 𝕂 𝔸 n evaluated at a fixed x equals the scalar multiple of x^n by 1/n!.

Русский

Переформулировка: функция n ↦ expSeries 𝕂 𝔸 n в точности x равна единице делённой на n! умноженной на x^n.

LaTeX

$$$\big(\lambda n, (\expSeries 𝕂 𝔸 n)\big) = (n! )^{-1} \cdot x^{n}$$$

Lean4

theorem expSeries_apply_eq (x : 𝔸) (n : ℕ) : (expSeries 𝕂 𝔸 n fun _ => x) = (n !⁻¹ : 𝕂) • x ^ n := by simp [expSeries]

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