totalDegree_le_degrees_card — Mathlib

English

The total degree of p is at most the number of distinct exponent vectors appearing, i.e., totalDegree(p) ≤ card(degrees(p)).

Русский

Общая степень p не превосходит число различных степеней, встречающихся; totalDegree(p) ≤ card(degrees(p)).

LaTeX

$$$\operatorname{totalDegree}(p) \le \lvert \operatorname{degrees}(p) \rvert$$$

Lean4

theorem totalDegree_le_degrees_card (p : MvPolynomial σ R) : p.totalDegree ≤ Multiset.card p.degrees := by
  classical
  rw [totalDegree_eq]
  exact Finset.sup_le fun s hs => Multiset.card_le_card <| Finset.le_sup hs

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