lean_workbook_plus_28648
ProvedWe know that , and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_28648 (x : ℝ) (hx : x = (1 + Real.sqrt 5) / 2) : x^2 = x + 1 ∧ 1/x = x - 1 := by sorry
Source
We know that , and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_28648 (x : ℝ) (hx : x = (1 + Real.sqrt 5) / 2) : x^2 = x + 1 ∧ 1/x = x - 1 := by sorry