analyticOnNhd_cexp — Mathlib

English

The complex exponential function is analytic on the whole complex plane.

Русский

Комплексная экспонента аналитична на всей плоскости комплексных чисел.

LaTeX

$$$ AnalyticOnNhd \mathbb{C} (\exp) (\\mathsf{univ}) $$$

Lean4

/-- The function `Complex.exp` is complex analytic. -/
theorem analyticOnNhd_cexp : AnalyticOnNhd ℂ exp univ :=
  by
  rw [Complex.exp_eq_exp_ℂ]
  exact fun x _ ↦ NormedSpace.exp_analytic x

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