mathlib3

4af7cb21 - feat(data/nat/choose/basic): Definition of `multichoose` and basic lemmas (#15072)

feat(data/nat/choose/basic): Definition of `multichoose` and basic lemmas (#15072) Defining `multichoose` which (by contrast with `choose`) counts the number of _multisets_ of cardinality `k` from a type of cardinality `n`, or equivalently the number of ways to select `k` items (up to permutation) from `n` items _with_ replacement. For eventual use in @huynhtrankhanh's #11162 ("stars and bars")