prod_X_sub_C_nextCoeff — Mathlib

English

For a multiset t of elements in R, the nextCoeff of the product ∏_{x∈t} (X − C x) equals −∑ x over t.

Русский

Для мультимножества t элементов R, nextCoeff от произведения ∏_{x∈t} (X − C x) равен − ∑ x по t.

LaTeX

$$$$\operatorname{nextCoeff}\left(\prod_{x\in t} (X - C x)\right) = -\sum_{x\in t} x.$$$$

Lean4

theorem prod_X_sub_C_nextCoeff {s : Finset ι} (f : ι → R) : nextCoeff (∏ i ∈ s, (X - C (f i))) = -∑ i ∈ s, f i := by
  simpa using multiset_prod_X_sub_C_nextCoeff (s.1.map f)

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