lean_workbook_plus_51031
ProvedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_51031 : 9 - 4 * Real.sqrt 5 = (2 - Real.sqrt 5) ^ 2 := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_51031 : 9 - 4 * Real.sqrt 5 = (2 - Real.sqrt 5) ^ 2 := by sorry