le_totalDegree — Mathlib

English

If s is in the support of p, then the sum of its coordinates is at most totalDegree(p).

Русский

Если s находится в опоре p, то сумма координат s не превышает totalDegree(p).

LaTeX

$$$\sum_i s_i \le \operatorname{totalDegree}(p) \quad\text{for any } s \in \operatorname{Supp}(p)$$$

Lean4

theorem le_totalDegree {p : MvPolynomial σ R} {s : σ →₀ ℕ} (h : s ∈ p.support) : (s.sum fun _ e => e) ≤ totalDegree p :=
  Finset.le_sup (α := ℕ) (f := fun s => sum s fun _ e => e) h

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