English
There is a natural equivalence between the n-th symmetric power of α and the set of finitely supported maps α → ℕ with total mass n.
Русский
Существует естественная эквивалентность между n-й симметрической степенью α и множеством функций α → ℕ с суммой массы n.
LaTeX
$$$$ \mathrm{Sym}(\alpha,n) \simeq \{ P : \alpha \to \mathbb{N} \mid P(\text{sum}) = n \}. $$$$
Lean4
/-- The `n`th symmetric power of a type `α` is naturally equivalent to the subtype of
finitely-supported maps `α →₀ ℕ` with total mass `n`.
See also `Sym.equivNatSumOfFintype` when `α` is finite. -/
def equivNatSum : Sym α n ≃ { P : α →₀ ℕ // P.sum (fun _ ↦ id) = n } :=
Multiset.toFinsupp.toEquiv.subtypeEquiv <| by simp
