Cosine_of_Sum
Provedaddition-formulasanalysisproofwikitrigonometry
cos(a+b) = cos(a)cos(b) - sin(a)sin(b).
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic theorem Cosine_of_Sum (a b : ℝ) : Real.cos (a + b) = Real.cos a * Real.cos b - Real.sin a * Real.sin b := by sorry
Source