Commit 2024-04-18 08:21 7bcbba0d

View on Github →

feat(NumberTheory/Harmonic): Euler-Mascheroni const = -Γ'(1) (#11611)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/Deriv/Shift.lean

added theorem deriv_comp_add_const

added theorem deriv_comp_const_add

Created Mathlib/NumberTheory/Harmonic/GammaDeriv.lean

added theorem Complex.deriv_Gamma_nat

added theorem Complex.differentiable_at_Gamma_nat_add_one

added theorem Complex.hasDerivAt_Gamma_nat

added theorem Complex.hasDerivAt_Gamma_one

added theorem Real.deriv_Gamma_nat

added theorem Real.eulerMascheroniConstant_eq_neg_deriv

added theorem Real.hasDerivAt_Gamma_nat

added theorem Real.hasDerivAt_Gamma_one