---
tag: 0TV07AQT62
kind: definition
name: Real exponentiation
msc: [26A09, 33B10]
defines: 091AV9YHZY
uses: [0RMVS7RXZX, 0044CPHJBV]
sources:
  - url: https://en.wikipedia.org/wiki/Exponentiation
    locator: Powers via logarithms
---

## Definition

Let $a > 0$ and let $x$ be a real number.
The power $a^x$ is
$$a^x = e^{x \ln a}.$$

## Remarks

For natural numbers $x = n$, this agrees with the product of $n$ factors $a$. For $x = p/q$, it agrees with $\sqrt[q]{a^p}$.
The usual rules hold: $a^{x + y} = a^x a^y$, $(a^x)^y = a^{x y}$, and $(a b)^x = a^x b^x$.
For $a = e$, it gives $e^x = \exp(x)$, since $\ln e = 1$. Mathlib defines `Real.rpow` with extra conventions for $a \le 0$.

## Explanations

### L1 human

To raise $a$ to a real power $x$, multiply the logarithm of $a$ by $x$ and apply the exponential function.
This fills in all powers between the rational ones continuously.