natDegree_eq_zero

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

natDegree p = 0 if and only if p is a constant polynomial.

Русский

natDegree p = 0 тогда и только тогда, когда p константный многочлен.

LaTeX

$$$ p.natDegree = 0 \leftrightarrow \exists x, C x = p. $$$

Lean4

theorem natDegree_eq_zero {p : R[X]} : p.natDegree = 0 ↔ ∃ x, C x = p :=
  ⟨fun h ↦ ⟨_, (eq_C_of_natDegree_eq_zero h).symm⟩, by aesop⟩

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

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

Разделы

Аффилиация

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