English
For a commutative semiring R and a finite type σ, esymm(s,n) is the nth elementary symmetric function of the multiset s, i.e., esymm(s,n) is the sum of the products of all n-element submultisets of s.
Русский
Для коммутативного полупругокольца R и конечного множества σ, esymm(s,n) есть n-ая элементарная симметрическая функция от элементов множества s: esymm(s,n) есть сумма произведений элементов по всем n-элементным подп Multiset s.
LaTeX
$$$ esymm (s : Multiset R) (n : \mathbb{N}) = ((s.powersetCard n).map Multiset.prod).sum $$$
Lean4
/-- The `n`th elementary symmetric function evaluated at the elements of `s` -/
def esymm (s : Multiset R) (n : ℕ) : R :=
((s.powersetCard n).map Multiset.prod).sum
