lean_workbook_plus_19213

Open

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

Prove that: $\sin(3x)=4\sin(x)\sin\left(\frac{\pi}{3}-x\right)\sin\left(\frac{\pi}{3}+x\right)$ using the complex exponential form $e^{ix}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19213 (x : ℝ) : Real.sin (3*x) = 4*Real.sin x * Real.sin (π/3 - x) * Real.sin (π/3 + x)   :=  by sorry

Source