lean_workbook_plus_63922

Proved

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

Solve the quadratic equation $x^2+6x=3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63922 (x : ℝ) : x^2 + 6*x = 3 ↔ x = -3 + 2*Real.sqrt 3 ∨ x = -3 - 2*Real.sqrt 3   :=  by sorry

Source