Real exponentiation

Summary

Real exponentiation defines the power $a^x$ for a positive base $a$ and a real exponent $x$. It is $e^{x \ln a}$, and it extends the powers with integer and rational exponents. The node real exponentiation gives the precise definition.