English
Let expSeries be the exponential series in a normed algebra. Then for every n, the n-th term evaluated at the constant zero function is the elementary delta: it equals 1 if n = 0 and 0 otherwise (i.e., the n-th term is the n-ary map that outputs 1 on the zero input only for n = 0, and 0 on all other inputs).
Русский
Пусть expSeries — экспоненциальная серия в нормированном алгебраическом пространстве. Тогда для любого n-ого члена expSeries, при подаче константной нулевой функции, получаем 1, если n = 0, и 0 иначе.
LaTeX
$$$(\\expSeries 𝕂 𝔸 n)(\\underbrace{0, \\dots, 0}_{n\\text{ times}}) = \\begin{cases} 1, & n=0, \\\\ 0, & n>0. \\end{cases}$$$
Lean4
theorem expSeries_apply_zero (n : ℕ) : expSeries 𝕂 𝔸 n (fun _ => (0 : 𝔸)) = Pi.single (M := fun _ => 𝔸) 0 1 n :=
by
rw [expSeries_apply_eq]
rcases n with - | n
· rw [pow_zero, Nat.factorial_zero, Nat.cast_one, inv_one, one_smul, Pi.single_eq_same]
· rw [zero_pow (Nat.succ_ne_zero _), smul_zero, Pi.single_eq_of_ne n.succ_ne_zero]
