lean_workbook_plus_28975
ProvedSo, which means
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_28975 (x : ℝ) : x^2 - 4*x + 2 = 0 ↔ x = 2 + Real.sqrt 2 ∨ x = 2 - Real.sqrt 2 := by sorry
Source
So, which means
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_28975 (x : ℝ) : x^2 - 4*x + 2 = 0 ↔ x = 2 + Real.sqrt 2 ∨ x = 2 - Real.sqrt 2 := by sorry