English
The n-th symmetric power of a finite type α is naturally equivalent to the subtype {P : α → ℕ | ∑ i P i = n} via equivNatSumOfFintype when α is finite.
Русский
Для конечного множества α естественно эквивалентно Sym α n множеству функций α → ℕ с суммой n через equivNatSumOfFintype.
LaTeX
$$$$ \text{equivNatSumOfFintype }\ α\ n : \mathrm{Sym}(\alpha,n) \simeq \{ P : \alpha \to \mathbb{N} \mid \sum i, P(i) = n \}, \quad [\text{Fintype }\alpha]. $$$$
Lean4
/-- The `n`th symmetric power of a finite type `α` is naturally equivalent to the subtype of maps
`α → ℕ` with total mass `n`.
See also `Sym.equivNatSum` when `α` is not necessarily finite. -/
noncomputable def equivNatSumOfFintype [Fintype α] : Sym α n ≃ { P : α → ℕ // ∑ i, P i = n } :=
(equivNatSum α n).trans <| Finsupp.equivFunOnFinite.subtypeEquiv <| by simp [Finsupp.sum_fintype]
