Commit 2024-02-13 14:05 8f463bc6

feat: Define general binomial coefficients (Ring.choose) (#9719) We define generalized binomial coefficients, and prove a couple basic properties. In particular, we show that multiplication by a suitable factorial yields a descending Pochhammer evaluation. We also show that casting Nat.choose is the same as taking Ring.choose of a natural number cast. To prove these, we add some results about polynomial evaluation.