English
For a multiset t of elements in R and ht: 0 < card t, (t.map (X − C x)).prod.coeff (card t − 1) = −t.sum.
Русский
Для мн-ва t элементов R и ht: 0 < card t, коэффициент произведения ∏_{x∈t} (X − C x) при степени card t − 1 равен − суммы t.
LaTeX
$$$$\text{card}(t) > 0 \implies \left(\prod_{x\in t} (X - C x)\right).\operatorname{coeff}(\operatorname{card}(t) - 1) = -\sum_{x\in t} x.$$$$
Lean4
theorem multiset_prod_X_sub_C_coeff_card_pred (t : Multiset R) (ht : 0 < Multiset.card t) :
(t.map fun x => X - C x).prod.coeff ((Multiset.card t) - 1) = -t.sum :=
by
nontriviality R
convert multiset_prod_X_sub_C_nextCoeff (by assumption)
rw [nextCoeff, if_neg]
swap
· rw [natDegree_multiset_prod_of_monic]
swap
· simp only [Multiset.mem_map]
rintro _ ⟨_, _, rfl⟩
apply monic_X_sub_C
simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map]
obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp ht
exact fun h => one_ne_zero <| h 1 ⟨_, ⟨x, hx, rfl⟩, natDegree_X_sub_C _⟩
congr; rw [natDegree_multiset_prod_of_monic] <;> · simp [monic_X_sub_C]
