exp_eq_tsum_div

Mathlib.Analysis.Normed.Algebra.Exponential

URI: https://scilib.ai/kg/mathlib#NormedSpace.exp_eq_tsum_div

English

The exponential equals the ts sum of x^n / n! for all x.

Русский

Экспонента равна сумме в смысле тсум по x^n / n! для всех x.

LaTeX

$$$\\exp 𝕂 = (x \\mapsto \\sum_{n=0}^{\\infty} \\dfrac{x^{n}}{n!})$$$

Lean4

theorem exp_eq_tsum_div : exp 𝕂 = fun x : 𝔸 => ∑' n : ℕ, x ^ n / n ! :=
  funext expSeries_sum_eq_div

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru