eraseLead_natDegree_le_aux

Mathlib.Algebra.Polynomial.EraseLead

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

English

(eraseLead f).natDegree ≤ f.natDegree.

Русский

(natDegree(eraseLead f)) ≤ natDegree(f).

LaTeX

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

Lean4

theorem eraseLead_natDegree_le_aux : (eraseLead f).natDegree ≤ f.natDegree :=
  natDegree_le_natDegree eraseLead_degree_le

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

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

Разделы

Аффилиация

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