mathlib3

5ec1572c - feat(nat/choose/central): definition of the central binomial coefficient, and bounds (#9753)

feat(nat/choose/central): definition of the central binomial coefficient, and bounds (#9753) Two exponential lower bounds on the central binomial coefficient. Co-authored-by: Johan Commelin <johan@commelin.net>