The other root of a quadratic

Proved

WorkbookSource.problem_15814

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Then $12x^2-17x+5=0$ . You can see pretty quickly that $1$ is a root, so synthetic division or whatever will get you $(x-1)(12x-5)=0$ . Obviously $x e 1$ , so $x=\frac{5}{12}$

Source: InternLM Lean-Workbook, record lean_workbook_15814 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_15814  (x : ℝ)
  (h₀ : 12 * x^2 - 17 * x + 5 = 0)
  (h₁ : x ≠ 1) :
  x = 5 / 12  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_15814; Apache-2.0

View graph