natTrailingDegree_le_of_mem_supp

Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

English

If a ∈ p.support, then natTrailingDegree(p) ≤ a.

Русский

Если a ∈ p.support, то natTrailingDegree(p) ≤ a.

LaTeX

$$\text{ If } a \in p.support, \; \operatorname{natTrailingDegree}(p) \le a$$

Lean4

theorem natTrailingDegree_le_of_mem_supp (a : ℕ) : a ∈ p.support → natTrailingDegree p ≤ a :=
  natTrailingDegree_le_of_ne_zero ∘ mem_support_iff.mp

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

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

Разделы

Аффилиация

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