Gamma_neg_nat_eq_zero — Mathlib

English

For any n ∈ ℕ, Γ(-n) = 0.

Русский

Для любого натурального n верно Γ(-n) = 0.

LaTeX

$$$\Gamma(-n) = 0 \quad (n\in\mathbb{N})$$$

Lean4

/-- At `-n` for `n ∈ ℕ`, the Gamma function is undefined; by convention we assign it the value `0`.
-/
theorem Gamma_neg_nat_eq_zero (n : ℕ) : Gamma (-n) = 0 := by
  simpa only [← Complex.ofReal_natCast, ← Complex.ofReal_neg, Complex.Gamma_ofReal, Complex.ofReal_eq_zero] using
    Complex.Gamma_neg_nat_eq_zero n

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