## Real logarithm

### Set

 context $x,b\in\mathbb R_+^*$ context $b\neq 1$ definiendum $\log_b(x):\mathbb R_+^*\to \mathbb R_+^*$ definiendum $\log_b(x):= y$ postulate $b^y=x$

The logarithm function is that of the Dimension

Consider

$\log_r(r^n/r^1) = \log_r(r^{n-1}) = n - 1 = \log_r(r^n) - \log_r(r^1)$

vs.

${\mathrm {dim}}({\mathbb R}^n/{\mathbb R}^1) = {\mathrm {dim}}({\mathbb R}^{n-1}) = n - 1 = {\mathrm {dim}}({\mathbb R}^n)-{\mathrm {dim}}({\mathbb R}^1)$

where by ${\mathbb R}^n/{\mathbb R}^1$ we mean a quotient vector space .

#### Theorems

$\log_\mathrm{e}=\mathrm{ln}$

#### Reference

Wikipedia: Exponentiation