English
Let f: σ → R and s a Finset σ. Then the nth elementary symmetric function of the multiset s mapped by f equals the sum over all n-element subsets t of s of the product of f over t.
Русский
Пусть f: σ → R и s — Finset σ. Тогда n-ая элементарная симметрическая функция от s, отображённого через f, равна сумме произведений f по всем n-элементным подмножествам t множества s.
LaTeX
$$$ (s.val.map f).esymm n = (s.powersetCard n s).sum (fun t => t.prod f) $$$
Lean4
theorem _root_.Finset.esymm_map_val {σ} (f : σ → R) (s : Finset σ) (n : ℕ) :
(s.val.map f).esymm n = (s.powersetCard n).sum fun t => t.prod f :=
by
simp only [esymm, powersetCard_map, ← Finset.map_val_val_powersetCard, map_map]
simp only [Function.comp_apply, Finset.prod_map_val, Finset.sum_map_val]
