degree_list_prod_le — Mathlib

English

For a list l of polynomials, the degree of the product is bounded by the sum of degrees.

Русский

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

LaTeX

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

Lean4

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

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