---
tag: 0E8HNVBCSP
kind: statement
role: theorem
name: Exponential of a sum
msc: [33B10]
uses: [0RMVS7RXZX, 0AN28XQ45Z]
sources:
  - url: https://en.wikipedia.org/wiki/Exponential_function
    locator: Functional equation
---

## Statement

For all real numbers $x$ and $y$,
$$\exp(x + y) = \exp(x) \exp(y).$$

## Remarks

Multiply the two series by the [[Cauchy product|0AN28XQ45Z]]. The binomial theorem gives $\sum_{k=0}^{n} \frac{x^k}{k!} \frac{y^{n-k}}{(n-k)!} = \frac{(x + y)^n}{n!}$.
In particular, $\exp(x) \exp(-x) = \exp(0) = 1$.
So $\exp$ is a group homomorphism from $(\mathbb{R}, +)$ to the multiplicative group $(0, \infty)$. Mathlib states the formula as `Real.exp_add`.

## Explanations

### L1 human

The exponential function turns addition into multiplication.
This is the rule $e^{x + y} = e^x e^y$ for powers.