lean_workbook_plus_5722
OpenThis is followed by the result.\n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5722 (a b : ℝ) : 2 * cos a * cos b = cos (a + b) + cos (a - b) := by sorry
Source
This is followed by the result.\n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_5722 (a b : ℝ) : 2 * cos a * cos b = cos (a + b) + cos (a - b) := by sorry