lean_workbook_plus_13675

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Correct the multiplication: $(\sqrt{5} + 3 + \sqrt{7})(\sqrt{5} + 3 - \sqrt{7})$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13675 : (Real.sqrt 5 + 3 + Real.sqrt 7) * (Real.sqrt 5 + 3 - Real.sqrt 7) = 7 + 6 * Real.sqrt 5   :=  by sorry

Source