eq_C_of_natDegree_eq_zero

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

If natDegree p = 0, then p = C (coeff p 0).

Русский

Если natDegree p = 0, то p = C(coeff p 0).

LaTeX

$$$ p.natDegree = 0 \Rightarrow p = C(p.coeff 0). $$$

Lean4

theorem eq_C_of_natDegree_eq_zero (h : natDegree p = 0) : p = C (coeff p 0) :=
  eq_C_of_natDegree_le_zero h.le

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

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

Разделы

Аффилиация

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