monic_prod_of_monic — Mathlib

English

If t is a finite set and f i are polynomials, and each f i is monic for i in t, then the product over i in t of f i is monic.

Русский

Если t — конечное множество и f i — полиномы, и каждый f i моноичен для i в t, то произведение по i в t является моноичным.

LaTeX

$$MonicProd: Monic(∏ i ∈ t, f i) given Monic(f i) for all i ∈ t.$$

Lean4

theorem monic_prod_of_monic (s : Finset ι) (f : ι → R[X]) (hs : ∀ i ∈ s, Monic (f i)) : Monic (∏ i ∈ s, f i) :=
  monic_multiset_prod_of_monic s.1 f hs

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