English
Let m be a multiset with card m = n. Then mk m h gives an element of Sym α n, i.e., a construction of the nth symmetric power from a multiset.
Русский
Пусть m — мультисет с card(m) = n. Тогда mk m h задаёт элемент Sym α n, то есть конструирует n-ю симметрическую мощность из мультисета.
LaTeX
$$$ mk(m,h) \in \mathrm{Sym}(\alpha,n) \\text{ with } h: \operatorname{card} m = n$$
Lean4
/-- Construct an element of the `n`th symmetric power from a multiset of cardinality `n`.
-/
@[match_pattern]
abbrev mk (m : Multiset α) (h : Multiset.card m = n) : Sym α n :=
⟨m, h⟩
