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