exp_eq_exp_ℂ — Mathlib

English

On the complex numbers, Complex.exp coincides with the exponential map coming from NormedSpace.exp for ℂ.

Русский

На комплексных числах Complex.exp совпадает с экспонентой, заданной через NormedSpace.exp для ℂ.

LaTeX

$$$$ \text{Complex.exp} = \text{NormedSpace.exp } \mathbb{C}. $$$$

Lean4

theorem exp_eq_exp_ℂ : Complex.exp = NormedSpace.exp ℂ :=
  by
  refine funext fun x => ?_
  rw [Complex.exp, exp_eq_tsum_div]
  exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable ℝ x).hasSum.tendsto_sum_nat

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