mathlib

a3209ddf - feat (special_functions/gamma): doubling formula (#19136)

feat (special_functions/gamma): doubling formula (#19136) This PR adds the proof of the Legendre doubling formula, relating `Gamma s * Gamma (s + 1 / 2)` to `Gamma (2 * s)`.