lean_workbook_plus_8864
ProvedCalculate .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8864 : (Real.sqrt 5 + 2) ^ 3 * (Real.sqrt 5 - 2) ^ 3 = 1 := by sorry
Source
Calculate .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_8864 : (Real.sqrt 5 + 2) ^ 3 * (Real.sqrt 5 - 2) ^ 3 = 1 := by sorry