lean_workbook_plus_48982

Proved

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

$1-(\frac{\sqrt{3}}{2})^2=1-\frac{3}{4}=\frac{1}{4}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_48982 :
  1 - (Real.sqrt 3 / 2)^2 = 1 / 4   :=  by sorry

Source