lean_workbook_plus_74029

Proved

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

Applying the quadratic formula again, find that that $z=\frac{6\pm\sqrt{36-4(3)(-9+4a)}}{2(3)}\implies z=\frac{6\pm\sqrt{144-48a}}{6}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74029 (a : ℝ) : (6 + Real.sqrt (36 - 4 * 3 * (-9 + 4 * a))) / (2 * 3) = (6 + Real.sqrt (144 - 48 * a)) / 6   :=  by sorry

Source