lean_workbook_plus_7888
ProvedSquaring both and gives and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7888 : (Real.sqrt 14)^2 = 14 ∧ (6 - Real.sqrt 3)^2 = 39 - 12 * Real.sqrt 3 := by sorry
Source
Squaring both and gives and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_7888 : (Real.sqrt 14)^2 = 14 ∧ (6 - Real.sqrt 3)^2 = 39 - 12 * Real.sqrt 3 := by sorry