cos pi = -1

Statement

$$\cos \pi = -1, \qquad \sin \pi = 0.$$

Remarks

By the definition of $\pi$, $\cos(\pi/2) = 0$. The Pythagorean identity gives $\sin(\pi/2) = 1$, since $\sin > 0$ on $(0, 2]$. The double angle formulas then give $\cos \pi = 2 \cos^2(\pi/2) - 1 = -1$ and $\sin \pi = 2 \sin(\pi/2) \cos(\pi/2) = 0$. Together with $\sin \pi = 0$, it gives Euler's identity $e^{i \pi} = -1$ in complex form. Mathlib states the first claim as Real.cos_pi.

Explanations

L1 human

Half a turn around the unit circle takes the point $(1, 0)$ to the point $(-1, 0)$. So $\cos \pi = -1$ and $\sin \pi = 0$.