Theorems · Definition · combinatorics

Sym.equivNatSum

(α : Type u_1) → [DecidableEq α] → (n : ℕ) → Sym α n ≃ { P // (P.sum fun x => id) = n }

The nth 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.

Defined in

Mathlib.Data.Finsupp.Multiset

Cited by

3 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq