cosh_add — Mathlib

English

The addition formula for complex cosh: cosh(x+y) = cosh x cosh y + sinh x sinh y.

Русский

Формула сложения для cosh: cosh(x+y) = cosh x cosh y + sinh x sinh y.

LaTeX

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

Lean4

theorem cosh_add : cosh (x + y) = cosh x * cosh y + sinh x * sinh y :=
  by
  rw [← mul_right_inj' (two_ne_zero' ℂ), two_cosh, exp_add, neg_add, exp_add, eq_comm, mul_add, ← mul_assoc, two_cosh, ←
    mul_assoc, two_sinh, ← mul_right_inj' (two_ne_zero' ℂ), mul_add, mul_left_comm, two_cosh, mul_left_comm, two_sinh]
  exact cosh_add_aux

Похожие утверждения