lean_workbook_plus_12049

Proved

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

Factor the quadratic equation $a^2+5ab+6b^2=0$ and solve for a and b.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12049 : ∀ a b : ℝ, a^2 + 5 * a * b + 6 * b^2 = 0 → (a + 2 * b) * (a + 3 * b) = 0   :=  by sorry

Source