Gamma_zero — Mathlib

English

For s ∈ ℂ and n ∈ ℕ with -Re(s) < n, ΓAux(n,s) = ΓAux(n,(s+1)) / s.

Русский

Для комплексного s и натурального n с условием -Re(s) < n, ΓAux(n,s) = ΓAux(n,(s+1)) / s.

LaTeX

$$$$ \GammaAux(n,s) = \dfrac{\GammaAux(n, s+1)}{s}, \quad -\operatorname{Re}(s) < n. $$$$

Lean4

/-- At `0` the Gamma function is undefined; by convention we assign it the value `0`. -/
@[simp]
theorem Gamma_zero : Gamma 0 = 0 := by simp_rw [Gamma, zero_re, sub_zero, Nat.floor_one, GammaAux, div_zero]

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