discrim_lt_zero_of_neg

Mathlib.Algebra.QuadraticDiscriminant

URI: https://scilib.ai/kg/mathlib#discrim_lt_zero_of_neg

← MathLib Explorer

English

If a ≠ 0 and a x^2 + b x + c < 0 for all x, then discrim a b c < 0.

Русский

Если a ≠ 0 и a x^2 + b x + c < 0 для всех x, дискриминант < 0.

LaTeX

$$$\mathrm{discrim}(a,b,c) < 0$$$

Lean4

theorem discrim_lt_zero_of_neg (ha : a ≠ 0) (h : ∀ x : K, a * (x * x) + b * x + c < 0) : discrim a b c < 0 :=
  discrim_neg a b c ▸ discrim_lt_zero (neg_ne_zero.2 ha) <| by simpa only [neg_mul, ← neg_add, neg_pos]

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

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

Разделы

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

Аффилиация

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