English
Let s be a finite multiset of elements of a commutative ring R. The product over t in s of (X − C t) expands as a polynomial in X, with coefficients given by elementary symmetric sums: ∑_{j=0}^{|s|} (−1)^j C(esymm_j(s)) X^{|s|−j}.
Русский
Пусть s — конечная мультисета элементов кольца R. Произведение по t∈s пары (X − C t) раскладывается в многочлик по степеням X; коэффициенты задаются элементарными симметрическими суммами: ∑_{j=0}^{|s|} (−1)^j C(esymm_j(s)) X^{|s|−j}.
LaTeX
$$$$ \\left( \\prod_{t \\in s} (X - C t) \\right) = \\sum_{j=0}^{|s|} (-1)^j \\, C\\big(s.esymm(j)\\big) \\, X^{|s| - j}. $$$$
Lean4
theorem prod_X_sub_X_eq_sum_esymm (s : Multiset R) :
(s.map fun t => X - C t).prod =
∑ j ∈ Finset.range (Multiset.card s + 1), (-1) ^ j * (C (s.esymm j) * X ^ (Multiset.card s - j)) :=
by
conv_lhs =>
congr
congr
ext x
rw [sub_eq_add_neg]
rw [← map_neg C x]
convert prod_X_add_C_eq_sum_esymm (map (fun t => -t) s) using 1
· rw [map_map]; rfl
· simp only [esymm_neg, card_map, mul_assoc, map_mul, map_pow, map_neg, map_one]
