mathlib

b76e9f65 - feat(analysis/special_functions/gamma): holomorphy of `1 / Gamma` (#19012)

feat(analysis/special_functions/gamma): holomorphy of `1 / Gamma` (#19012) This PR makes two changes to the Gamma function code: - drastically shorten the proof of differentiability of the Gamma function by applying general results on Mellin transforms; - add the fact that `1 / Gamma` is differentiable everywhere (including at the poles of the Gamma function).