Gamma — Mathlib

English

The Gamma function is meromorphic on the entire complex plane (univ).

Русский

Функция гамма мероморфна на всей комплексной плоскости (на всём множесте).

LaTeX

$$$\text{MeromorphicNFOn}(\Gamma, \mathbb{C}, \text{univ})$$$

Lean4

theorem Gamma : MeromorphicNFOn Gamma univ :=
  meromorphicNFOn_inv.mp <|
    AnalyticOnNhd.meromorphicNFOn <| analyticOnNhd_univ_iff_differentiable.mpr differentiable_one_div_Gamma

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