natDegree_list_sum_le — Mathlib

English

For a list of polynomials l, the degree of the sum is at most the maximum of the degrees of the summands.

Русский

Степень суммы полиномов не превосходит максимальную степень слагаемых.

LaTeX

$$natDegree (l.sum) ≤ max { natDegree p | p ∈ l }$$

Lean4

theorem natDegree_list_sum_le (l : List S[X]) : natDegree l.sum ≤ (l.map natDegree).foldr max 0 :=
  by
  apply List.sum_le_foldr_max natDegree
  · simp
  · exact natDegree_add_le

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