card_supp_le_succ_natDegree — Mathlib · SciLib

English

The size of the support is at most natDegree(p) + 1: |supp(p)| ≤ natDegree(p) + 1.

Русский

Размер опорной поддержки не превосходит natDegree(p) плюс 1.

LaTeX

$$$|\operatorname{supp}(p)| \le \operatorname{natDegree}(p) + 1.$$$

Lean4

theorem card_supp_le_succ_natDegree (p : R[X]) : #p.support ≤ p.natDegree + 1 :=
  by
  rw [← Finset.card_range (p.natDegree + 1)]
  exact Finset.card_le_card supp_subset_range_natDegree_succ

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