English
Let s be a finite multiset of elements of a commutative ring R and k ≤ |s|. Then the coefficient of X^k in the product ∏_{t∈s} (X − C t) equals (−1)^{|s|−k} esymm(|s|−k).
Русский
Пусть s — конечная мультисета элементов кольца R и k ≤ |s|. Тогда коэффициент при X^k в произведении ∏_{t∈s} (X − C t) равен (−1)^{|s|−k} esymm(|s|−k).
LaTeX
$$$$ \\Big( \\prod_{t \\in s} (X - C t) \\Big).coeff\_k = (-1)^{|s|-k} \\operatorname{esymm}\\big(|s|-k\\big). $$$$
Lean4
theorem prod_X_sub_C_coeff (s : Multiset R) {k : ℕ} (h : k ≤ Multiset.card s) :
(s.map fun t => X - C t).prod.coeff k = (-1) ^ (Multiset.card s - k) * s.esymm (Multiset.card s - k) :=
by
conv_lhs =>
congr
congr
congr
ext x
rw [sub_eq_add_neg]
rw [← map_neg C x]
convert prod_X_add_C_coeff (map (fun t => -t) s) _ using 1
· rw [map_map]; rfl
· rw [esymm_neg, card_map]
· rwa [card_map]
