eraseLead_degree_le

Mathlib.Algebra.Polynomial.EraseLead

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

English

degree of eraseLead(f) is at most degree of f.

Русский

Степень eraseLead(f) не превосходит степени f.

LaTeX

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

Lean4

theorem eraseLead_degree_le : (eraseLead f).degree ≤ f.degree :=
  f.degree_erase_le _

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

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

Разделы

Аффилиация

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