lean_workbook_plus_81280

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If $a>0$ and $b^2-4ac<0$ then $ax^2+bx+c>0$ for all value of $x$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81280 (a b c x: ℝ) (ha : a > 0) (h : b^2 - 4 * a * c < 0) : a * x^2 + b * x + c > 0   :=  by sorry

Source