degreeOf_sum_le — Mathlib

English

Same as previous: degree bound for sums via supremum over indices.

Русский

То же, что и выше: ограничение степени по сумме через наибольшую степень по суммируемым частям.

LaTeX

$$$\deg_i\left(\sum_{j\in s} f_j\right) \le \max_{j\in s} \deg_i(f_j)$$$

Lean4

theorem degreeOf_sum_le {ι : Type*} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R) :
    degreeOf i (∑ j ∈ s, f j) ≤ s.sup fun j => degreeOf i (f j) :=
  by
  simp_rw [degreeOf_eq_sup]
  exact supDegree_sum_le

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