coeff_zero_prod — Mathlib

English

For a finite index set s and polynomials f_i ∈ R[X], coeff((∏ i∈s f_i), 0) = ∏ i∈s coeff(f_i, 0).

Русский

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

LaTeX

$$$$\operatorname{coeff}\left( \prod_{i\in s} f_i, 0 \right) = \prod_{i\in s} \operatorname{coeff}(f_i, 0).$$$$

Lean4

theorem coeff_zero_prod : (∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0 := by
  simpa using coeff_zero_multiset_prod (s.1.map f)

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