ThmDex – An index of mathematical definitions, results, and conjectures.
F9908
Formulation 0
Let $x \mapsto \log x$ be the D865: Standard natural real logarithm function.
Then \begin{equation} \log 1 = 0 \end{equation}