English
For a list of polynomials l, the degree of the sum is bounded by the maximum of their natDegree values.
Русский
Степень суммы полиномов списка ограничена максимумом значений natDegree для элементов списка.
LaTeX
$$degree (l.sum) ≤ (l.map natDegree).maximum$$
Lean4
theorem degree_list_sum_le (l : List S[X]) : degree l.sum ≤ (l.map natDegree).maximum :=
by
apply degree_list_sum_le_of_forall_degree_le
intro p hp
by_cases h : p = 0
· subst h
simp
· rw [degree_eq_natDegree h]
apply List.le_maximum_of_mem'
rw [List.mem_map]
use p
simp [hp]