lean_workbook_plus_8581

Proved

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

Are $\frac{18}{17}+\frac{6\sqrt3}{17}$ and $\frac{18+6\sqrt3}{17}$ considered equivalent answers?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8581 (x : ℝ) : (18 / 17 + 6 * Real.sqrt 3 / 17) = (18 + 6 * Real.sqrt 3) / 17   :=  by sorry

Source