Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-03 09:48 6e26cff9

View on Github →

feat(analysis/special_functions): add the Gamma function (#12917)

Estimated changes

Created src/analysis/special_functions/gamma.lean

added def complex.Gamma_integral

added theorem complex.Gamma_integral_convergent

added theorem complex.Gamma_integral_of_real

added theorem complex.Gamma_integral_one

added theorem integral_exp_neg_Ioi

added def real.Gamma_integral

added theorem real.Gamma_integral_convergent

added theorem real.Gamma_integral_one

added theorem real.Gamma_integrand_is_O