lean_workbook_plus_7240

Open

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

$\sin{x}\sin{y}=\frac{1}{2}\cdot\left[\cos{\left(x-y\right)}-\cos{\left(x+y\right)}\right]$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7240 : ∀ x y : ℝ, sin x * sin y = 1 / 2 * (cos (x - y) - cos (x + y))   :=  by sorry

Source