degree_le_zero_iff

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

degree p ≤ 0 iff p = C(coeff p 0).

Русский

degree p ≤ 0 эквивалентно p = C(coeff p 0).

LaTeX

$$$ degree(p) \le 0 \iff p = C (coeff(p,0)) $$$

Lean4

theorem degree_le_zero_iff : degree p ≤ 0 ↔ p = C (coeff p 0) :=
  ⟨eq_C_of_degree_le_zero, fun h => h.symm ▸ degree_C_le⟩

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

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

Разделы

Аффилиация

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