degree_list_sum_le_of_forall_degree_le

English

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

Русский

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

LaTeX

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

Lean4

theorem degree_list_sum_le_of_forall_degree_le (l : List S[X]) (n : WithBot ℕ) (hl : ∀ p ∈ l, degree p ≤ n) :
    degree l.sum ≤ n := by
  induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [List.mem_cons, forall_eq_or_imp] at hl
    rcases hl with ⟨hhd, htl⟩
    rw [List.sum_cons]
    exact le_trans (degree_add_le hd tl.sum) (max_le hhd (ih htl))

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