degree_quadratic_le

Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

← MathLib Explorer

English

Let a ≠ 0. Then deg(C(a)·X^2 + C(b)·X + C(c)) ≤ 2.

Русский

Пусть a ≠ 0. Тогда deg(C(a)·X^2 + C(b)·X + C(c)) ≤ 2.

LaTeX

$$$\deg(C(a)\,X^2 + C(b)\,X + C(c)) \le 2 \quad(a \neq 0)$$$

Lean4

theorem degree_quadratic_le : degree (C a * X ^ 2 + C b * X + C c) ≤ 2 := by
  simpa only [add_assoc] using
    degree_add_le_of_degree_le (degree_C_mul_X_pow_le 2 a)
      (le_trans degree_linear_le <| WithBot.coe_le_coe.mpr one_le_two)

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

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

Разделы

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

Аффилиация

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