natDegree_pos_of_eraseLead_ne_zero

Mathlib.Algebra.Polynomial.EraseLead

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

← MathLib Explorer

English

If eraseLead(f) ≠ 0 then 0 < f.natDegree.

Русский

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

LaTeX

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

Lean4

theorem natDegree_pos_of_eraseLead_ne_zero (h : f.eraseLead ≠ 0) : 0 < f.natDegree :=
  by
  by_contra h₂
  rw [eq_C_of_natDegree_eq_zero (Nat.eq_zero_of_not_pos h₂)] at h
  simp at h

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

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

Разделы

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

Аффилиация

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