degree_le_two

Mathlib.Analysis.Complex.Polynomial.Basic

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

← MathLib Explorer

English

If a real polynomial p is irreducible, then its degree is at most 2.

Русский

Пусть p ∈ ℝ[X] неразложимый. Тогда deg p ≤ 2.

LaTeX

$$$\\\\deg p \\\\le 2$$$

Lean4

/-- An irreducible real polynomial has degree at most two. -/
theorem degree_le_two {p : ℝ[X]} (hp : Irreducible p) : degree p ≤ 2 :=
  natDegree_le_iff_degree_le.1 hp.natDegree_le_two

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

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

Разделы

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

Аффилиация

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