degree_pos

Mathlib.Algebra.Polynomial.FieldDivision

URI: https://scilib.ai/kg/mathlib#Irreducible.degree_pos

← MathLib Explorer

English

An irreducible polynomial over a field must have positive degree.

Русский

Неразложимый многочлен над полем имеет положительную степень.

LaTeX

$$$0 < f.degree$ for irreducible f.$$

Lean4

/-- An irreducible polynomial over a field must have positive degree. -/
theorem degree_pos (h : Irreducible f) : 0 < f.degree :=
  by
  rw [← natDegree_pos_iff_degree_pos]
  exact h.natDegree_pos

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

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

Разделы

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

Аффилиация

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