Commit 2024-03-14 11:12 7f38ed7c

View on Github →

feat: the nth symmetric power is equivalent to maps of total mass n. (#11360)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

added theorem Multiset.sum_count_eq

Modified Mathlib/Data/Finsupp/Multiset.lean

added theorem Multiset.toFinsupp_sum_eq

added theorem Sym.coe_equivNatSumOfFintype_apply_apply

added theorem Sym.coe_equivNatSumOfFintype_symm_apply

added theorem Sym.coe_equivNatSum_apply_apply

added theorem Sym.coe_equivNatSum_symm_apply

added def Sym.equivNatSum