degree_multiset_prod_le — Mathlib

English

For a multiset t of polynomials, the natDegree of the product is at most the sum of natDegrees of elements.

Русский

Степень произведения полиномов в мультимножестве не превосходит суммы степеней элементов.

LaTeX

$$natDegree (t.prod) ≤ (t.map natDegree).sum$$

Lean4

/-- The degree of a product of polynomials is at most the sum of the degrees,
where the degree of the zero polynomial is ⊥.
-/
theorem degree_multiset_prod_le : t.prod.degree ≤ (t.map Polynomial.degree).sum :=
  Quotient.inductionOn t (by simpa using degree_list_prod_le)

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