[Merged by Bors] - feat: the nth symmetric power is equivalent to maps of total mass n.

[ocfnash]

---

[eric-wieser]

If you pass this through DFinsupp.equivFunOnFintype and Finsupp.toDFinsupp, then it would be computable, which is nice for #eval

[ocfnash]

If it could be rendered computable for free I would do it, but I think even the low price of having to depend on DFinsupp.equivFunOnFintype (incidentally not imported in this file) makes it not worth it for me (especially as it's really just accident that we have computable DFinsupp.equivFunOnFintype and noncomputable Finsupp.equivFunOnFinite).

[eric-wieser]

Perhaps the better resolution here is to have a Multiset.countEquiv or similar that is the Fintype analog to Multiset.toFinsupp, with a nice defeq for the summation. I'll let you decide if that sounds out of scope

bors d+

[ocfnash]

I guess we should probably have this somewhere:

def Multiset.countAddEquiv (α : Type*) [Fintype α] [DecidableEq α] :
    Multiset α ≃+ (α → ℕ) where
  toFun s := s.count
  invFun P := ∑ a, P a • {a}
  map_add' s t := by ext; simp
  left_inv s := by
    ext a
    change count a (sum _) = _
    rw [count_sum]
    simp [count_singleton]
  right_inv P := by
    ext a
    change count a (sum _) = _
    rw [count_sum]
    simp [count_singleton]

I'll try to come back to this (in a separate PR).

[mathlib-bors]

✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ocfnash]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style