Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-14 09:06 79827670

View on Github →

chore(analysis/special_functions/gamma): split into 3 files (#19004) This PR splits the existing 1500-line file analysis.special_functions.gamma into 3 files. There are no changes to the content of the files (other than top-of-file docstrings and imports).

Estimated changes

deleted def complex.Gamma
deleted theorem complex.Gamma_add_one
deleted theorem complex.Gamma_conj
deleted theorem complex.Gamma_eq_integral
deleted theorem complex.Gamma_eq_zero_iff
deleted theorem complex.Gamma_ne_zero
deleted theorem complex.Gamma_of_real
deleted theorem complex.Gamma_one
deleted theorem complex.Gamma_seq_mul
deleted theorem complex.Gamma_zero
deleted def dGamma_integrand
deleted def real.Gamma
deleted theorem real.Gamma_add_one
deleted theorem real.Gamma_eq_integral
deleted theorem real.Gamma_eq_zero_iff
deleted theorem real.Gamma_integrand_is_o
deleted theorem real.Gamma_ne_zero
deleted theorem real.Gamma_one
deleted theorem real.Gamma_pos_of_pos
deleted theorem real.Gamma_two
deleted theorem real.Gamma_zero
deleted theorem real.convex_on_Gamma
deleted theorem real.convex_on_log_Gamma
added def complex.Gamma
added theorem complex.Gamma_add_one
added theorem complex.Gamma_conj
added theorem complex.Gamma_of_real
added theorem complex.Gamma_one
added theorem complex.Gamma_zero
added def dGamma_integrand
added def real.Gamma
added theorem real.Gamma_add_one
added theorem real.Gamma_eq_integral
added theorem real.Gamma_eq_zero_iff
added theorem real.Gamma_ne_zero
added theorem real.Gamma_one
added theorem real.Gamma_pos_of_pos
added theorem real.Gamma_zero
added theorem complex.Gamma_ne_zero
added theorem complex.Gamma_seq_mul
added theorem real.Gamma_two
added theorem real.convex_on_Gamma