degrees_prod_le — Mathlib

English

For a finite set s and f: s → MvPolynomial, deg(∏_{i∈s} f(i)) ≤ ∑_{i∈s} deg(f(i)).

Русский

Для конечного множества s и функции f: s → MvPolynomial, deg(∏_{i∈s} f(i)) ≤ ∑_{i∈s} deg(f(i)).

LaTeX

$$$\deg\left(\prod_{i \in s} f(i)\right) \le \sum_{i \in s} \deg\left(f(i)\right)$$$

Lean4

theorem degrees_prod_le {ι : Type*} {s : Finset ι} {f : ι → MvPolynomial σ R} :
    (∏ i ∈ s, f i).degrees ≤ ∑ i ∈ s, (f i).degrees := by classical exact supDegree_prod_le (map_zero _) (map_add _)

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