degree_list_sum_le — Mathlib

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]

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