lean_workbook_plus_43951
OpenSolve for :
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_43951 : x^2 - 2*x - 1 = 0 ↔ x = 1 + Real.sqrt 2 ∨ x = 1 - Real.sqrt 2 := by sorry
Source
Solve for :
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_43951 : x^2 - 2*x - 1 = 0 ↔ x = 1 + Real.sqrt 2 ∨ x = 1 - Real.sqrt 2 := by sorry