eraseLead_natDegree_le

Mathlib.Algebra.Polynomial.EraseLead

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

← MathLib Explorer

English

(eraseLead f).natDegree ≤ f.natDegree − 1

Русский

(natDegree(eraseLead f)) ≤ natDegree(f) − 1.

LaTeX

$$$\operatorname{natDegree}(\operatorname{eraseLead}(f)) \le \operatorname{natDegree}(f) - 1$$$

Lean4

theorem eraseLead_natDegree_le (f : R[X]) : (eraseLead f).natDegree ≤ f.natDegree - 1 :=
  by
  rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with (h | h)
  · exact Nat.le_sub_one_of_lt h
  · simp only [h, natDegree_zero, zero_le]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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