prod — Mathlib

English

A product of monic polynomials is monic.

Русский

Произведение моничных полиномов является моничным.

LaTeX

$$$$ m.Monic\left(\prod_{i\in s} P_i\right) \\text{if } m.Monic(P_i) \text{ for all } i \in s. $$$$

Lean4

/-- A product of monic polynomials is monic -/
protected theorem prod {ι : Type*} {P : ι → MvPolynomial σ R} {s : Finset ι} (H : ∀ i ∈ s, m.Monic (P i)) :
    m.Monic (∏ i ∈ s, P i) := by
  rw [Monic, leadingCoeff_prod_of_regular]
  · exact Finset.prod_eq_one H
  · intro i hi
    rw [(H i hi).leadingCoeff_eq_one]
    exact isRegular_one

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