multiset_prod_X_sub_C_nextCoeff — Mathlib

English

For a multiset t of polynomials and a natural n, if natDegree(p) ≤ n for all p ∈ t, then coeff(t.prod, |t|·n) = ∏_{p∈t} coeff(p, n).

Русский

Для мультимножества t полиномов и натурального n, если natDegree(p) ≤ n для каждого p ∈ t, то коэффициент произведения при степени |t|·n равен произведению коэффициентов p при n.

LaTeX

$$$$\left( \forall p \in t, \operatorname{natDegree}(p) \le n \right) \implies \operatorname{coeff}\left( \prod_{p\in t} p, |t| \cdot n \right) = \prod_{p\in t} \operatorname{coeff}(p, n).$$$$

Lean4

theorem multiset_prod_X_sub_C_nextCoeff (t : Multiset R) : nextCoeff (t.map fun x => X - C x).prod = -t.sum :=
  by
  rw [nextCoeff_multiset_prod]
  · simp only [nextCoeff_X_sub_C]
    exact t.sum_hom (-AddMonoidHom.id R)
  · intros
    apply monic_X_sub_C

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