degree_pos_of_irreducible

Mathlib.Algebra.Polynomial.FieldDivision

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

← MathLib Explorer

English

If p is irreducible in R[X], then 0 < degree p.

Русский

Если p ирредуцируем, то 0 < deg p.

LaTeX

$$Irreducible p → 0 < p.degree$$

Lean4

theorem degree_pos_of_irreducible (hp : Irreducible p) : 0 < p.degree :=
  lt_of_not_ge fun hp0 =>
    have := eq_C_of_degree_le_zero hp0
    not_irreducible_C (p.coeff 0) <| this ▸ hp

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

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

Разделы

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

Аффилиация

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