lean_workbook_plus_72962

Proved

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

Solve the equation: \n\n

\frac{x+a+1}{x}=a-x\implies {{x}^{2}}-(a-1)x+a+1=0

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72962 {x a : ℝ} (h₁ : x ≠ 0) (h₂ : a = 7) : (x + a + 1) / x = a - x ↔ x^2 - (a - 1) * x + a + 1 = 0   :=  by sorry

Source