degree_quadratic

Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

← MathLib Explorer

English

If 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

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

Lean4

@[simp]
theorem degree_quadratic (ha : a ≠ 0) : degree (C a * X ^ 2 + C b * X + C c) = 2 :=
  by
  rw [add_assoc, degree_add_eq_left_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha, degree_C_mul_X_pow 2 ha]
  rfl

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

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

Разделы

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

Аффилиация

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