natDegree_sum_le_of_forall_le — Mathlib

English

The degree of a sum is bounded by the maximum of the degrees of summands.

Русский

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

LaTeX

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

Lean4

theorem natDegree_sum_le_of_forall_le {n : ℕ} (f : ι → S[X]) (h : ∀ i ∈ s, natDegree (f i) ≤ n) :
    natDegree (∑ i ∈ s, f i) ≤ n :=
  le_trans (natDegree_sum_le s f) <| (Finset.fold_max_le n).mpr <| by simpa

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