lean_workbook_plus_31418

Proved

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

For this particular problem, $3 = \frac {s\sqrt {3}}{2}\quad\Longrightarrow\quad s = 2\sqrt {3}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31418 (s : ℝ) : 3 = s * Real.sqrt 3 / 2 → s = 2 * Real.sqrt 3   :=  by sorry

Source