lean_workbook_plus_2535
OpenProve the following identity.\n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2535 : ∀ x : ℝ, Real.cos (2 * x) = 2 * (Real.cos x)^2 - 1 := by sorry
Source
Prove the following identity.\n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2535 : ∀ x : ℝ, Real.cos (2 * x) = 2 * (Real.cos x)^2 - 1 := by sorry