lean_workbook_plus_4399
Openprove
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_4399 (a : ℝ) : Real.cos (3 * a) = 4 * (Real.cos a)^3 - 3 * Real.cos a := by sorry
Source
prove
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_4399 (a : ℝ) : Real.cos (3 * a) = 4 * (Real.cos a)^3 - 3 * Real.cos a := by sorry