prod_X_add_C_coeff' — Mathlib

English

For a finite set s and function r, the product ∏_{i∈s} (X+ C(r_i)) has coefficient k equal to esymm(|s|-k)(r-values).

Русский

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

LaTeX

$$$$\\left(\\prod_{i\\in s} (X + C(r_i))\\right)_{X^k} = \\mathrm{esymm}_{|s|-k}(r_i).$$$$

Lean4

theorem prod_X_add_C_coeff' {σ} (s : Multiset σ) (r : σ → R) {k : ℕ} (h : k ≤ Multiset.card s) :
    (s.map fun i => X + C (r i)).prod.coeff k = (s.map r).esymm (Multiset.card s - k) := by
  rw [← Function.comp_def (f := fun r => X + C r) (g := r), ← map_map, prod_X_add_C_coeff] <;> rw [s.card_map r];
  assumption

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