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