exp — Mathlib

English

The exponential power series exp in A is defined by coefficients (algebraMap from ℚ to A) of 1/n!; i.e., exp_A = ∑_{n≥0} (1/n!) X^n mapped into A.

Русский

Степенной ряд экспоненты exp в кольце A определяется коэффициентами из ℚ в A: 1/n! при X^n.

LaTeX

$$$$ \mathrm{exp}\, A := \mathrm{mk}\, (n \mapsto \alpha_n) \quad\text{with } \alpha_n = \text{algebraMap }\mathbb{Q} A \left(\frac{1}{n!}\right) $$$$

Lean4

/-- Power series for the exponential function at zero. -/
def exp : PowerSeries A :=
  mk fun n => algebraMap ℚ A (1 / n !)

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