natDegree_list_prod_le — Mathlib

English

For a list l of polynomials, the natDegree of the product is bounded by the sum of natDegrees.

Русский

Степень произведения полиномов в списке ограничена суммой степеней каждого элемента.

LaTeX

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

Lean4

theorem natDegree_list_prod_le (l : List S[X]) : natDegree l.prod ≤ (l.map natDegree).sum := by
  induction l with
  | nil => simp
  | cons hd tl IH => simpa using natDegree_mul_le.trans (add_le_add_left IH _)

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