Gamma_neg_nat_eq_zero — Mathlib

English

For natural 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
  induction n with
  | zero => rw [Nat.cast_zero, neg_zero, Gamma_zero]
  | succ n
    IH =>
    have A : -(n.succ : ℂ) ≠ 0 := by
      rw [neg_ne_zero, Nat.cast_ne_zero]
      apply Nat.succ_ne_zero
    have : -(n : ℂ) = -↑n.succ + 1 := by simp
    rw [this, Gamma_add_one _ A] at IH
    contrapose! IH
    exact mul_ne_zero A IH

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