eq_C_of_degree_eq_zero

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

If deg p = 0 then p = C(coeff p 0).

Русский

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

LaTeX

$$$ p \in R[X],\; degree(p) = 0 \Rightarrow p = C (coeff(p,0)) $$$

Lean4

theorem eq_C_of_degree_eq_zero (h : degree p = 0) : p = C (coeff p 0) :=
  eq_C_of_degree_le_zero h.le

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

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

Разделы

Аффилиация

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