English
For a type α and natural number n, the nth symmetric power Sym α n is the set of multisets of size n drawn from α, i.e. the subtype of Multiset α consisting of those with cardinality n.
Русский
Порядковая n-я симметрическая степень Sym α n есть множество многочленов из α размером n, то есть подмножество Multiset α состоящее из элементов с кардинальностью n.
LaTeX
$$$\\mathrm{Sym}\\;\\alpha\\;n = \\{\,s : \\mathrm{Multiset}(\\alpha) \\,\\mid\\, \\mathrm{card}(s) = n\,\\}$$$
Lean4
/-- The nth symmetric power is n-tuples up to permutation. We define it
as a subtype of `Multiset` since these are well developed in the
library. We also give a definition `Sym.sym'` in terms of vectors, and we
show these are equivalent in `Sym.symEquivSym'`.
-/
def Sym (α : Type*) (n : ℕ) :=
{ s : Multiset α // Multiset.card s = n }
deriving [DecidableEq α] → DecidableEq _
