lean_workbook_plus_6481

Proved

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

Our numbers are roots of the equation $x^2-2ax+a^2-1=0$ , or $(x-a)^2=1 \implies x_1=a-1,x_2=a+1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6481 (a : ℝ) : a-1 ∈ {x | x^2 - 2*a*x + a^2 - 1 = 0} ∧ a+1 ∈ {x | x^2 - 2*a*x + a^2 - 1 = 0}   :=  by sorry

Source