expSeries_apply_eq_div — Mathlib

English

The n-th term of the expSeries on the constant x equals x^n / n!.

Русский

n-ый член expSeries при константном x равен x^n / n!.

LaTeX

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

Lean4

theorem expSeries_apply_eq_div (x : 𝔸) (n : ℕ) : (expSeries 𝕂 𝔸 n fun _ => x) = x ^ n / n ! := by
  rw [div_eq_mul_inv, ← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq, ← smul_eq_mul, expSeries_apply_eq,
    inv_natCast_smul_eq 𝕂 𝔸]

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