degree_erase_lt — Mathlib

English

If p is nonzero, then deleting its natDegree term strictly lowers the degree.

Русский

Если p ≠ 0, то удаление элемента с натуральной нормой ведёт к меньшей степени.

LaTeX

$$$p \neq 0 \rightarrow \deg(p.erase(\operatorname{natDegree}(p))) < \deg(p)$$$

Lean4

theorem degree_erase_lt (hp : p ≠ 0) : degree (p.erase (natDegree p)) < degree p :=
  by
  apply lt_of_le_of_ne (degree_erase_le _ _)
  rw [degree_eq_natDegree hp, degree, support_erase]
  exact fun h => notMem_erase _ _ (mem_of_max h)

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