degree_of_a_eq_zero

Mathlib.Algebra.CubicDiscriminant

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

English

If the cubic has a = 0, then the degree of the associated polynomial is at most 2.

Русский

Если коэффициент при X^3 равен нулю, то степень соответствующего полинома не превышает 2.

LaTeX

$$$\\deg(P.toPoly) \\le 2 \\quad\\text{when } P.a = 0$$$

Lean4

theorem degree_of_a_eq_zero (ha : P.a = 0) : P.toPoly.degree ≤ 2 := by
  simpa only [of_a_eq_zero ha] using degree_quadratic_le

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

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

Разделы

Аффилиация

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