le_natDegree_of_mem_supp — Mathlib

English

Let p be a polynomial over a semiring R. If a is a natural number that appears with a nonzero coefficient in p, then a ≤ natDegree(p).

Русский

Пусть p — полином над полускольной полусистемой R. Если а ∈ supp(p) и a ∈ ℕ, то a не превосходит natDegree(p).

LaTeX

$$$\forall p \in R[X], \forall a \in \mathbb{N},\ a \in \operatorname{supp}(p)\Rightarrow a \le \operatorname{natDegree}(p).$$$

Lean4

theorem le_natDegree_of_mem_supp (a : ℕ) : a ∈ p.support → a ≤ natDegree p :=
  le_natDegree_of_ne_zero ∘ mem_support_iff.mp

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