nextCoeff_prod — Mathlib

English

For a finite set s and f, nextCoeff of the product over s equals the sum of nextCoeff of each f i.

Русский

Для конечного множества s и функции f, nextCoeff произведения равен сумме nextCoeff каждого f i.

LaTeX

$$Monic.nextCoeff_prod: nextCoeff(∏ i ∈ s, f i) = ∑ i ∈ s, nextCoeff(f i)$$

Lean4

theorem nextCoeff_prod (s : Finset ι) (f : ι → R[X]) (h : ∀ i ∈ s, Monic (f i)) :
    nextCoeff (∏ i ∈ s, f i) = ∑ i ∈ s, nextCoeff (f i) :=
  Monic.nextCoeff_multiset_prod s.1 f h

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