totalDegree_list_prod — Mathlib

English

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

Русский

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

LaTeX

$$$\operatorname{totalDegree}\left(\prod_{i} p_i\right) \le \sum_i \operatorname{totalDegree}(p_i)$$$

Lean4

theorem totalDegree_list_prod : ∀ s : List (MvPolynomial σ R), s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum
  | [] => by rw [List.prod_nil, totalDegree_one, List.map_nil, List.sum_nil]
  | p :: ps => by
    rw [List.prod_cons, List.map, List.sum_cons]
    exact le_trans (totalDegree_mul _ _) (add_le_add_left (totalDegree_list_prod ps) _)

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