expSeries_radius_pos

Mathlib.Analysis.Normed.Algebra.Exponential

URI: https://scilib.ai/kg/mathlib#NormedSpace.expSeries_radius_pos

English

The radius of convergence is strictly greater than zero.

Русский

Радиус сходимости строго положителен.

LaTeX

$$$ 0 < (\operatorname{expSeries} 𝕂 𝔸).radius $$$

Lean4

theorem expSeries_radius_pos : 0 < (expSeries 𝕂 𝔸).radius :=
  by
  rw [expSeries_radius_eq_top]
  exact WithTop.top_pos

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

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

Разделы

Аффилиация

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