coeff_zero_multiset_prod — Mathlib

English

For a multiset t of polynomials, coeff(t.prod, 0) equals the product of coeff(p,0) for p ∈ t.

Русский

Для мультимножества t полиномов коэффициент при степени 0 у произведения равен произведению коэффициентов коэффициентов при 0 каждого полинома.

LaTeX

$$$$\operatorname{coeff}\left( t.prod, 0 \right) = \prod_{p \in t} \operatorname{coeff}(p, 0).$$$$

Lean4

theorem coeff_zero_multiset_prod : t.prod.coeff 0 = (t.map fun f => coeff f 0).prod :=
  by
  refine Multiset.induction_on t ?_ fun a t ht => ?_; · simp
  rw [Multiset.prod_cons, Multiset.map_cons, Multiset.prod_cons, Polynomial.mul_coeff_zero, ht]

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