lean_workbook_plus_68742

Open

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

$cosh(x+y) = cosh(x)cosh(y) + sinh(x)sinh(y)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source