lean_workbook_plus_4699

Proved

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

Solving the square: \nIf there is an equation $ax^2+bx+c=0$ , \nThen you can simplify to $x^2+\frac{bx}{a}+\frac{c}{a}=0$ \nThe property $(x+a)^2=x^2+2a+a^2$ becomes relevant, because we can substitute $a$ in this equation with $\frac{b}{2a}$ , thus getting \n $(x+\frac{b}{2a})^2=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4699  (a b c x : ℝ)
  (h₀ : a ≠ 0)
  (h₁ : a * x^2 + b * x + c = 0) :
  x^2 + b / a * x + c / a = 0   :=  by sorry

Source

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

View graph