exp — Mathlib

English

The complex exponential function exp is defined as the limit of its Taylor partial sums exp'(z).

Русский

Комплексная экспонента exp определяется как предел её частичных сумм Тейлора exp'(z).

LaTeX

$$$\\exp(z) = \\lim_{n\\to\\infty} \\left( \\sum_{m=0}^{n-1} \\frac{z^m}{m!} \\right)$$$

Lean4

/-- The complex exponential function, defined via its Taylor series -/
@[pp_nodot]
def exp (z : ℂ) : ℂ :=
  CauSeq.lim (exp' z)

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