degreeOf_mul_le — Mathlib

English

Degree of i in a finite sum is at most the supremum over the summands: deg_i(∑ j∈s f_j) ≤ sup_j deg_i(f_j).

Русский

Степень i в конечной сумме не больше верхней грани степеней суммируемых элементов.

LaTeX

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

Lean4

theorem degreeOf_mul_le (i : σ) (f g : MvPolynomial σ R) : degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g := by
  classical
  simp only [degreeOf]
  convert Multiset.count_le_of_le i degrees_mul_le
  rw [Multiset.count_add]

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