Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-24 15:29 c9e2f055

View on Github →

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.

Estimated changes

added theorem finset.sym_fill_mem
added theorem finset.sum_pow
added theorem finsupp.multinomial_eq
added theorem nat.multinomial_congr
modified theorem sym.coe_append
added theorem sym.coe_fill
added theorem sym.fill_filter_ne
added theorem sym.filter_ne_fill
modified theorem sym.mem_fill_iff
modified theorem sym.sigma_sub_ext