mathlib

954896a1 - feat(data/nat/choose/cast): Cast of binomial coefficients equals a Pochhammer polynomial (#9394)

feat(data/nat/choose/cast): Cast of binomial coefficients equals a Pochhammer polynomial (#9394) This adds some glue between `nat.factorial`/`nat.asc_factorial`/`nat.desc_factorial` and `pochhammer` to provide some API to calculate binomial coefficients in a semiring. For example, `n.choose 2` as a real is `n * (n - 1)/2`. I also move files as such: * create `data.nat.choose.cast` * create `data.nat.factorial.cast` * rename `data.nat.factorial` to `data.nat.factorial.basic`