theorem proved term proof

`cos_dAlembert_to_ODE`

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

formal statement (Lean)

 259theorem cos_dAlembert_to_ODE : dAlembert_to_ODE_hypothesis_neg Real.cos := by

Term-mode proof.

 260  intro _ _ _ _
 261  exact cos_second_deriv_eq
 262
 263/-- cos satisfies the d'Alembert equation. -/

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

cos_satisfies_regularity in IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation decl_use

Lean names referenced from this declaration's body.

cos_second_deriv_eq in IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation decl_use
dAlembert_to_ODE_hypothesis_neg in IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation decl_use