lean_workbook_plus_81481

Proved

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

lean_workbooktrivial

The equation $x^2+ax+2b = 0$ has real roots when $a^2-8b\ge{0}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81481 (a b : ℝ) (h : a^2 - 8 * b ≥ 0) : ∃ x, x^2 + a * x + 2 * b = 0   :=  by sorry

Source