lean_workbook_plus_1832

Proved

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

Solving the equation for x gives us $x^2 - 18x + 65 = 0$ , which factors to $(x-13)(x-5) = 0.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1832 (x : ℝ) (hx : x^2 - 18*x + 65 = 0) : (x-13)*(x-5) = 0   :=  by sorry

Source