English
Let s be a finite multiset of elements of a commutative ring R. For every nonnegative integer k, the k-th elementary symmetric sum of the negated multiset −s equals (−1)^k times the k-th elementary symmetric sum of s.
Русский
Пусть s — конечная мультисета элементов кольца R. Для каждого неотрицательного целого k сумма, состоящая из симметрических комбинаций элементов −s взятая по рангу k, равна (−1)^k умноженному на k-ю элементарную симметрическую сумму множества s.
LaTeX
$$$$ \\operatorname{esymm}(-s, k) = (-1)^k \\operatorname{esymm}(s, k). $$$$
Lean4
theorem esymm_neg (s : Multiset R) (k : ℕ) : (map Neg.neg s).esymm k = (-1) ^ k * esymm s k :=
by
rw [esymm, esymm, ← Multiset.sum_map_mul_left, Multiset.powersetCard_map, Multiset.map_map, map_congr rfl]
intro x hx
rw [(mem_powersetCard.mp hx).right.symm, ← prod_replicate, ← Multiset.map_const]
nth_rw 3 [← map_id' x]
rw [← prod_map_mul, map_congr rfl, Function.comp_apply]
exact fun z _ => neg_one_mul z
