Gamma_eq_zero_iff — Mathlib

English

The Gamma function vanishes exactly at negative integers (if real argument).

Русский

Функция Гамма ноль точно на целых отрицательных числах (для вещественных аргументов).

LaTeX

$$$\Gamma(s) = 0 \iff \exists m:\mathbb{N}, s = -m$$$

Lean4

theorem Gamma_eq_zero_iff (s : ℝ) : Gamma s = 0 ↔ ∃ m : ℕ, s = -m :=
  ⟨by contrapose!; exact Gamma_ne_zero, by rintro ⟨m, rfl⟩; exact Gamma_neg_nat_eq_zero m⟩

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