totalDegree_finset_prod — Mathlib

English

For a finite set of polynomials, the total degree of the product is at most the sum of their degrees.

Русский

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

LaTeX

$$$\operatorname{totalDegree}(\prod_{i \in s} f(i)) \le \sum_{i \in s} \operatorname{totalDegree}(f(i))$$$

Lean4

theorem totalDegree_finset_prod {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) :
    (s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree :=
  by
  refine le_trans (totalDegree_multiset_prod _) ?_
  simp only [Multiset.map_map, comp_apply, Finset.sum_map_val, le_refl]

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