totalDegree_multiset_prod — Mathlib

English

For a multiset of polynomials, the total degree of the product is bounded by the sum of their total degrees.

Русский

Для мультисета полиномов общая степень произведения ограничена суммой их общих степеней.

LaTeX

$$$\operatorname{totalDegree}(\prod s) \le \sum_{p \in s} \operatorname{totalDegree}(p)$$$

Lean4

theorem totalDegree_multiset_prod (s : Multiset (MvPolynomial σ R)) :
    s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum :=
  by
  refine Quotient.inductionOn s fun l => ?_
  rw [Multiset.quot_mk_to_coe, Multiset.prod_coe, Multiset.map_coe, Multiset.sum_coe]
  exact totalDegree_list_prod l

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