mathlib

c9e2f055 - feat(data/nat/choose/multinomial): add multinomial theorem (#16317)

feat(data/nat/choose/multinomial): add multinomial theorem (#16317) Proof by induction on the number of summands. finset.sym is used to sum over. It means we have access to the finset tooling to rewrite it, and it's one of the more direct ways of expressing it. Co-authored-by: Pim Otte <potte@quintor.nl> Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>