lean_workbook_plus_14676
OpenProve that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14676 : ∀ x y z : ℝ, sin (x + y) * sin (y + z) = sin y * sin (x + y + z) + sin z * sin x := by sorry
Source
Prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14676 : ∀ x y z : ℝ, sin (x + y) * sin (y + z) = sin y * sin (x + y + z) + sin z * sin x := by sorry