---
tag: 0S049HG1W5
kind: statement
role: corollary
name: Power-reduction formula for cosine
msc: [33B10]
uses: [028XEQCE88, 03H7WZ4T3K]
sources:
  - url: https://en.wikipedia.org/wiki/List_of_trigonometric_identities
    locator: Power-reduction formula
---

## Statement

For every real $x$,
$$\cos^2 x = \frac{1 + \cos 2x}{2}, \qquad \sin^2 x = \frac{1 - \cos 2x}{2}.$$

## Remarks

The [[addition formula|028XEQCE88]] gives $\cos 2x = \cos^2 x - \sin^2 x$. With the [[Pythagorean identity|03H7WZ4T3K]], $\cos 2x = 2 \cos^2 x - 1 = 1 - 2 \sin^2 x$.
These formulas give $\int_0^{\pi} \cos^2 x \, dx = \frac{\pi}{2}$.
Mathlib states the first one as `Real.cos_sq`.

## Explanations

### L1 human

A square of a cosine is a cosine of the double angle, shifted and scaled.
This turns squares into first powers, which are easy to integrate.