Integral of cosine

Statement

For all real numbers $a$ and $b$, $$\int_a^b \cos x \, dx = \sin b - \sin a.$$

Remarks

The derivative of sine is $\cos$, so $\sin$ is an antiderivative of $\cos$. For example, $\int_0^{\pi/2} \cos x \, dx = 1$. Mathlib states it as integral_cos.

Explanations

L1 human

The sine function is an antiderivative of the cosine function. So the integral of cosine is a difference of two sine values.