le_weightedTotalDegree — Mathlib

English

If a monomial d appears in the support of a polynomial φ, then weight w d is bounded above by the weighted total degree of φ.

Русский

Если моном d встречается в поддержке многочлена φ, то весовая величина weight w d не превосходит взвешенную суммарную степень φ.

LaTeX

$$$\\text{weight } w d \\; \\leq \\text{weightedTotalDegree}(w,\\varphi)\\quad\\text{whenever } d \\in \\mathrm{support}(\\varphi)$$$

Lean4

theorem le_weightedTotalDegree (w : σ → M) {φ : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : d ∈ φ.support) :
    weight w d ≤ φ.weightedTotalDegree w :=
  le_sup hd

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