no goals
R : Type u
ι : Type w
s✝ : Finset ι
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < Finset.card s
⊢ coeff (∏ i in s, (X - ↑C (f i))) (Finset.card s - 1) = -∑ i in s, f i
simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using hs)
no goals
R : Type u
ι : Type w
s✝ : Finset ι
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < Finset.card s
⊢ 0 < ↑Multiset.card (Multiset.map f s.val)
simpa using hs