le_degree_of_mem_supp

Mathlib.Algebra.Polynomial.Degree.Support

URI: https://scilib.ai/kg/mathlib#Polynomial.le_degree_of_mem_supp

English

If a ∈ p.support, then a ≤ degree p (i.e., the exponent a does not exceed the degree of p).

Русский

Если a ∈ поддержка(p), то a ≤ degree(p).

LaTeX

$$$a \in \operatorname{supp}(p) \Rightarrow a \le \operatorname{degree}(p).$$$

Lean4

theorem le_degree_of_mem_supp (a : ℕ) : a ∈ p.support → ↑a ≤ degree p :=
  le_degree_of_ne_zero ∘ mem_support_iff.mp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru