prod_X_sub_C_coeff_card_pred — Mathlib

English

For a finite set s, a function f, and hs: 0 < card s, (∏ i∈s (X − C(f i))).coeff (card s − 1) = −∑ i∈s f i.

Русский

Для конечного множества s и функции f, при условии 0 < card s, коэффициент при степени card s − 1 в произведении ∏_{i∈s} (X − C(f i)) равен −∑ f i.

LaTeX

$$$$\operatorname{coeff}\left( \prod_{i\in s} (X - C(f(i))), |s| - 1 \right) = -\sum_{i\in s} f(i).$$$$

Lean4

theorem prod_X_sub_C_coeff_card_pred (s : Finset ι) (f : ι → R) (hs : 0 < #s) :
    (∏ i ∈ s, (X - C (f i))).coeff (#s - 1) = -∑ i ∈ s, f i := by
  simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using hs)

Похожие утверждения