lean_workbook_plus_10621

Proved

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

D is the discriminant, or the part of the quadratic formula under the square root. The discriminant determines if a quadratic has a repeated solution, two real ones, or two complex ones. $D=b^2-4ac$ . When it is plugged into $-\dfrac{D}{4a}$ , you get $c-\dfrac{b^2}{4a}$ , which was in NivekUil's formula for the maximum (the $y$ -coordinate of the vertex).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10621  (a b c : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = a * x^2 + b * x + c)
  (h₁ : a ≠ 0) :
  -(b^2 - 4 * a * c) / (4 * a) = c - b^2 / (4 * a)   :=  by sorry

Source

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

View graph