lean_workbook_plus_59732

Proved

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

$\frac{3}{\sqrt7}=\frac{3\sqrt7}{7}$ , $\frac{2}{\sqrt6}=\frac{\sqrt6}{3}$ . Subtract to get $\frac{9\sqrt7-7\sqrt6}{21}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59732 :
  3 / Real.sqrt 7 - 2 / Real.sqrt 6 = (9 * Real.sqrt 7 - 7 * Real.sqrt 6) / 21   :=  by sorry

Source