deriv_Gamma_nat — Mathlib

English

For every natural n, the derivative of the complex Gamma at n+1 equals n!(-γ + H_n).

Русский

Для каждого натурального n производная комплексной Gamma в точке n+1 равна n!(-γ + H_n).

LaTeX

$$$\operatorname{deriv} \Gamma (n+1) = n!\,(-\gamma + H_n)$$$

Lean4

/-- Explicit formula for the derivative of the complex Gamma function at positive integers, in
terms of harmonic numbers and the Euler-Mascheroni constant `γ`. -/
theorem deriv_Gamma_nat (n : ℕ) : deriv Gamma (n + 1) = n ! * (-γ + harmonic n) :=
  (hasDerivAt_Gamma_nat n).deriv

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