Complex exponents with positive real bases

Function

context $ b\in\mathbb R_+^* $
definiendum $ z\mapsto b^z :\mathbb C\to\mathbb C $
definiendum $ z\mapsto b^z := \mathrm{exp}(z\cdot \mathrm{ln}(b)) $

Discussion

The identity

$b^{x_1+x_2}=b^{x_1}\cdot a^{x_2}$,

says that exponentiation is a (the) homomorphism between $+$ and $\cdot$.

The combinatorial manifestation, e.g. formulated in for $B,X_1,X_2,\dots\in\bf{Set}$, is

$B^{\coprod_{j\in J}X_j}\cong\prod_{j\in J} B^{X_j}$


Context

Natural logarithm of real numbers