pith. machine review for the scientific record. sign in
theorem proved term proof

cos_dAlembert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 264theorem cos_dAlembert : ∀ t u, Real.cos (t+u) + Real.cos (t-u) = 2 * Real.cos t * Real.cos u := by

proof body

Term-mode proof.

 265  intro t u
 266  rw [Real.cos_add, Real.cos_sub]
 267  ring
 268
 269/-- **Main Theorem (d'Alembert Cosine Solution)**:
 270
 271d'Alembert equation + calibration H''(0) = -1 ⟹ H = cos.
 272
 273This is the "Angle T5" theorem, parallel to the "Cost T5" theorem
 274`dAlembert_cosh_solution` in `Cost.FunctionalEquation`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.