ThmDex – An index of mathematical definitions, results, and conjectures.
F9892
Formulation 2
The standard natural real logarithm function is the D4364: Real function \begin{equation} \log : (0, \infty) \to \mathbb{R}, \quad \log(x) = \int^x_1 t^{-1} \, d t \end{equation}