Commit 2024-05-25 20:06 9248805d

View on Github →

feat (NumberTheory/Harmonic): compute Gamma'(1/2) (#12923) Show Gamma'(1/2) = -√π * (γ + 2 * log 2) and various other related results.

Estimated changes

Modified Mathlib/NumberTheory/Harmonic/GammaDeriv.lean

modified theorem Complex.hasDerivAt_Gamma_one

added theorem Complex.hasDerivAt_Gamma_one_half

added theorem Complex.hasDerivAt_Gammaℂ_one

added theorem Complex.hasDerivAt_Gammaℝ_one

modified theorem Real.eulerMascheroniConstant_eq_neg_deriv

modified theorem Real.hasDerivAt_Gamma_one

added theorem Real.hasDerivAt_Gamma_one_half