eq_X_add_C

Mathlib.Algebra.Polynomial.Degree.SmallDegree

URI: https://scilib.ai/kg/mathlib#Polynomial.Monic.eq_X_add_C

← MathLib Explorer

English

If p is monic and natDegree p = 1, then p = X + C(p.coeff 0).

Русский

Если p монический и natDegree p = 1, то p = X + C(p.coeff 0).

LaTeX

$$$\text{If } p\text{ is monic and }\operatorname{natDegree}(p)=1:\; p = X + C(p_{0}).$$$

Lean4

theorem eq_X_add_C (hm : p.Monic) (hnd : p.natDegree = 1) : p = X + C (p.coeff 0) := by
  rw [← one_mul X, ← C_1, ← hm.coeff_natDegree, hnd, ← eq_X_add_C_of_natDegree_le_one hnd.le]

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

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

Разделы

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

Аффилиация

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