sinh_add — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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