lean_workbook_plus_59414

Proved

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

Solve for $k$ in the equation $2k - 3 = \frac{1}{4}k^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59414 (k : ℝ) : 2 * k - 3 = 1 / 4 * k ^ 2 ↔ k = 2 ∨ k = 6   :=  by sorry

Source