lean_workbook_plus_50659

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that $\sinh(x+y)=\sinh(x)\cosh(y)+\sinh(y)\cosh(x)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50659 (x y : ℝ) : sinh (x + y) = sinh x * cosh y + sinh y * cosh x   :=  by sorry

Source