English
The nth term of the exponential series, applied to n copies of x, equals (1/n!) times x^n.
Русский
Член n-й экспоненциальной серии, применённый к n копиям x, равен (1/n!) умноженному на x^n.
LaTeX
$$$(\expSeries 𝕂 𝔸 n) (x,\dots,x) = (n!)^{-1} \cdot x^{n}$$$
Lean4
/-- `NormedSpace.exp 𝕂 : 𝔸 → 𝔸` is the exponential map determined by the action of `𝕂` on `𝔸`.
It is defined as the sum of the `FormalMultilinearSeries` `expSeries 𝕂 𝔸`.
Note that when `𝔸 = Matrix n n 𝕂`, this is the **Matrix Exponential**; see
[`MatrixExponential`](./Mathlib/Analysis/Normed/Algebra/MatrixExponential) for lemmas
specific to that case. -/
noncomputable def exp (x : 𝔸) : 𝔸 :=
(expSeries 𝕂 𝔸).sum x
