Derivatives of the hyperbolic functions

Statement

The functions $\sinh$, $\cosh$ and $\tanh$ are differentiable on $\mathbb{R}$, and for every real $x$ $$\sinh'(x) = \cosh x, \qquad \cosh'(x) = \sinh x, \qquad \tanh'(x) = \frac{1}{\cosh^2 x} = 1 - \tanh^2 x.$$

Remarks

The first two follow from $\exp' = \exp$ and $(e^{-x})' = -e^{-x}$. The third follows from the quotient rule and the identity $\cosh^2 - \sinh^2 = 1$. So $\sinh'' = \sinh$ and $\cosh'' = \cosh$. Mathlib states the first one as Real.hasDerivAt_sinh.

Explanations

L1 human

Unlike sine and cosine, there is no minus sign here. Each of $\sinh$ and $\cosh$ is the derivative of the other.