degree_cubic_lt

Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

← MathLib Explorer

English

degree of a cubic is less than 4: deg(C(a)·X^3 + C(b)·X^2 + C(c)·X + C(d)) < 4.

Русский

Степень кубического полинома меньше 4: deg(C(a)·X^3 + C(b)·X^2 + C(c)·X + C(d)) < 4.

LaTeX

$$$\deg(C(a)\,X^3 + C(b)\,X^2 + C(c)\,X + C(d)) < 4 \quad(ha \neq 0)$$$

Lean4

theorem degree_cubic_lt : degree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) < 4 :=
  degree_cubic_le.trans_lt <| WithBot.coe_lt_coe.mpr <| lt_add_one 3

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

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

Разделы

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

Аффилиация

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