---
tag: 028XEQCE88
kind: statement
role: theorem
name: Angle addition formulas
msc: [33B10]
uses: [0WB57D9488, 0AN28XQ45Z]
sources:
  - url: https://en.wikipedia.org/wiki/List_of_trigonometric_identities
    locator: Angle sum and difference identities
---

## Statement

For all real numbers $x$ and $y$,
$$\sin(x + y) = \sin x \cos y + \cos x \sin y,$$
$$\cos(x + y) = \cos x \cos y - \sin x \sin y.$$

## Remarks

One proof multiplies the power series with the [[Cauchy product|0AN28XQ45Z]] and uses the binomial theorem.
Another proof fixes $y$ and shows that the difference of the two sides solves $f'' = -f$ with $f(0) = f'(0) = 0$.
With $y = x$, they give $\sin 2x = 2 \sin x \cos x$ and $\cos 2x = \cos^2 x - \sin^2 x$. Mathlib states them as `Real.sin_add` and `Real.cos_add`.

## Explanations

### L1 human

These formulas compute the sine and cosine of a sum of two angles from the sines and cosines of the angles.
They are the most important trigonometric identities.