prod_X_add_C_coeff — Mathlib

English

For a finite set s ⊆ σ and function r, the Finset version of coeff: (∏_{i∈s} (X+ C(r_i))).coeff k equals esymm(|s|-k) of (r_i).

Русский

Для конечного множества s и функции r, коэффициент k произведения равен esymm(|s|-k)(r_i).

LaTeX

$$$$\\bigg(\\prod_{i\\in s} (X + C(r_i))\\bigg)\\text{ coeff } k = \\mathrm{esymm}_{|s|-k}(r_i).$$$$

Lean4

theorem _root_.Finset.prod_X_add_C_coeff {σ} (s : Finset σ) (r : σ → R) {k : ℕ} (h : k ≤ #s) :
    (∏ i ∈ s, (X + C (r i))).coeff k = ∑ t ∈ s.powersetCard (#s - k), ∏ i ∈ t, r i :=
  by
  rw [Finset.prod, prod_X_add_C_coeff' _ r h, Finset.esymm_map_val]
  rfl

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