mathlib

a280c1e5 - feat(data/nat/{choose/multinomial,factorial/big_operations}): add multinomial coefficient definition with basic lemma's (#16170)

feat(data/nat/{choose/multinomial,factorial/big_operations}): add multinomial coefficient definition with basic lemma's (#16170) Chose a definition based on finset and a function for multiplicity. This allows the definition to be used in various context, including in a multiset context, where multiset.count yields the function describing multiplicity. Supporting lemma's concerning factorials are introduced in a new file, since importing big_operators in the main factorial file yields a circular import. Co-authored-by: Kyle Miller <kmill31415@gmail.com>