analyticOn_cexp

Mathlib.Analysis.SpecialFunctions.ExpDeriv

URI: https://scilib.ai/kg/mathlib#analyticOn_cexp

English

The function exp is complex analytic on the entire plane.

Русский

Функция exp является комплексно-аналитической во всей плоскости.

LaTeX

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

Lean4

/-- The function `Complex.exp` is complex analytic. -/
theorem analyticOn_cexp : AnalyticOn ℂ exp univ :=
  analyticOnNhd_cexp.analyticOn

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru