degree_eraseLead_lt

Mathlib.Algebra.Polynomial.EraseLead

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

English

If f ≠ 0, then degree of eraseLead(f) is strictly less than degree of f.

Русский

Если f ≠ 0, то deg(eraseLead(f)) < deg(f).

LaTeX

$$$f \neq 0 \Rightarrow \deg(\operatorname{eraseLead}(f)) < \deg(f)$$$

Lean4

theorem degree_eraseLead_lt (hf : f ≠ 0) : (eraseLead f).degree < f.degree :=
  f.degree_erase_lt hf

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

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

Разделы

Аффилиация

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