degree_linear_lt

Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

English

For a linear polynomial p = C(a)·X + C(b), its degree is less than 2; i.e., degree(p) < 2.

Русский

Для линейного полинома p = C(a)·X + C(b) их степень меньше 2.

LaTeX

$$$\deg(C(a)\,X + C(b)) < 2$$$

Lean4

theorem degree_linear_lt : degree (C a * X + C b) < 2 :=
  degree_linear_le.trans_lt <| WithBot.coe_lt_coe.mpr one_lt_two

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

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

Разделы

Аффилиация

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