mathlib

2c15ce14 - feat(data/nat/choose): add facts about the multiplicity of primes in the factorisation of central binomial coefficients (#9925)

feat(data/nat/choose): add facts about the multiplicity of primes in the factorisation of central binomial coefficients (#9925) A number of bounds on the multiplicity of primes in the factorisation of central binomial coefficients. These are of interest because they form part of the proof of Bertrand's postulate. Co-authored-by: Johan Commelin <johan@commelin.net>