Commit 2024-07-29 07:19 29fe1f7e

View on Github →

feat: The multinomial theorem in terms of piAntidiag (#14998) Prove that (∑ i in s, f i) ^ n = ∑ k in piAntidiag s n, multinomial s k * ∏ i in s, f i ^ k i. We already have a version of this for Finset.sym, so I am also adding machinery to deduce one from the other. I however haven't managed to do that. From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

added theorem Multiset.mem_sum

modified theorem Multiset.sum_count_eq

added theorem Multiset.sum_count_eq_card

Modified Mathlib/Algebra/Order/Antidiag/Pi.lean

added theorem Finset.map_sym_eq_piAntidiag

Modified Mathlib/Data/Multiset/Basic.lean

added theorem Multiset.count_injective

modified theorem Multiset.mem_nsmul

added theorem Multiset.mem_nsmul_of_ne_zero

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

added theorem Finset.sum_pow_eq_sum_piAntidiag

added theorem Finset.sum_pow_eq_sum_piAntidiag_of_commute

modified theorem Finset.sum_pow_of_commute

Modified Mathlib/Data/Sym/Basic.lean

added theorem Sym.coe_mk

added theorem Sym.«exists»

added theorem Sym.«forall»