discrim_le_zero_of_nonpos — Mathlib

English

If a polynomial a x^2 + b x + c is always nonpositive, then discrim a b c ≤ 0.

Русский

Если квадратный многочлен всегда неположителен, то дискриминант неположителен.

LaTeX

$$$\forall x\; a x^2 + b x + c \le 0 \Rightarrow \mathrm{discrim}(a,b,c) \le 0$$$

Lean4

theorem discrim_le_zero_of_nonpos (h : ∀ x : K, a * (x * x) + b * x + c ≤ 0) : discrim a b c ≤ 0 :=
  discrim_neg a b c ▸ discrim_le_zero <| by simpa only [neg_mul, ← neg_add, neg_nonneg]

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