lean_workbook_plus_54511

Proved

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

Given a quadratic function $f(x) = ax^2 + bx + c$ , where $a \neq 0$ and $\Delta = b^2 - 4ac \geq 0$ , factor $f(x)$ using the quadratic formula.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54511 (a b c x : ℝ) (ha : a ≠ 0) (h : b^2 - 4 * a * c ≥ 0) : a * x^2 + b * x + c = a * (x - (-b + Real.sqrt (b^2 - 4 * a * c)) / (2 * a)) * (x - (-b - Real.sqrt (b^2 - 4 * a * c)) / (2 * a))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph