---
tag: 0WB57D9488
kind: definition
name: Sine and cosine
msc: [33B10, 26A09]
defines: 08WFZP6P89
uses: [0VP56B4EMX, 02KTRHQMHN, 08W5RN375X]
sources:
  - url: https://en.wikipedia.org/wiki/Sine_and_cosine
    locator: Series and polynomials
---

## Definition

The sine and cosine functions $\sin, \cos \colon \mathbb{R} \to \mathbb{R}$ are defined by the power series
$$\sin x = \sum_{n=0}^{\infty} \frac{(-1)^n x^{2n+1}}{(2n+1)!}, \qquad \cos x = \sum_{n=0}^{\infty} \frac{(-1)^n x^{2n}}{(2n)!}.$$

## Remarks

Both [[series|02KTRHQMHN]] [[converge|08W5RN375X]] absolutely for every real $x$.
Sine is odd and cosine is even. Also $\sin 0 = 0$ and $\cos 0 = 1$.
Geometrically, $(\cos x, \sin x)$ is the point of the unit circle at arc length $x$ from $(1, 0)$, counterclockwise.
Mathlib defines `Real.sin` and `Real.cos` from the complex exponential, with $\cos x + i \sin x = e^{i x}$.

## Explanations

### L1 human

Sine and cosine describe motion around the unit circle.
In analysis, we define them by power series, and we then prove their geometric properties.