degree_of_c_eq_zero

Mathlib.Algebra.CubicDiscriminant

URI: https://scilib.ai/kg/mathlib#Cubic.degree_of_c_eq_zero

← MathLib Explorer

English

If a = 0, b = 0 and c = 0, then deg ≤ 0.

Русский

Если a = 0, b = 0 и c = 0, deg не превышает 0.

LaTeX

$$$a=0 \\land b=0 \\land c=0 \\Rightarrow \\deg((0,0,0,d).toPoly) \\le 0$$$

Lean4

theorem degree_of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.toPoly.degree ≤ 0 := by
  simpa only [of_c_eq_zero ha hb hc] using degree_C_le

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

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

Разделы

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

Аффилиация

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