Let $x \mapsto \log(x)$ be the D865: Standard natural real logarithm function.
The standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$ is the D5482: Positive real function \begin{equation} \log_a : (0, \infty) \to \mathbb{R}, \quad \log_a(x) = \frac{\log x}{\log a} \end{equation}