lean_workbook_plus_78674
OpenPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78674 (x y : ℝ) : sin x - sin y = 2 * cos ((x + y) / 2) * sin ((x - y) / 2) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_78674 (x y : ℝ) : sin x - sin y = 2 * cos ((x + y) / 2) * sin ((x - y) / 2) := by sorry