Formal exponential

Let $𝕂$ be a field with $c h a r 𝕂 = 0$ . The formal exponential refers to purely formal usage of the exponential function as a power series, i.e. $e x p 𝑧 \in 𝕂 [[𝑧]] \leq 𝕂 {𝑧}$ is defined by #m/def/fcalc

e x p 𝑧 = \sum 𝑛 \in ℕ 0 𝑧 𝑛 𝑛!

#state/develop | #lang/en | #SemBr