Angle between two vectors

Definition

Let $n$ be a positive integer, and let $u$ and $v$ be nonzero vectors in $\mathbb{R}^n$. Let $u \cdot v = u_1 v_1 + \dots + u_n v_n$ be their dot product, and let $\|u\|$ and $\|v\|$ be their lengths. The angle between $u$ and $v$ is the unique real number $\theta$ with $0 \leq \theta \leq \pi$ such that $$\cos \theta = \frac{u \cdot v}{\|u\| \, \|v\|}.$$ The Cauchy–Schwarz inequality $|u \cdot v| \leq \|u\| \, \|v\|$ makes sure that the quotient is in $[-1, 1]$. Thus $\theta = \arccos\left(\frac{u \cdot v}{\|u\| \, \|v\|}\right)$ exists.

Remarks

The angle is $0$ if and only if $v = c u$ for a real number $c > 0$. It is $\pi$ if and only if $v = c u$ for a real number $c < 0$. The angle does not depend on the order of the vectors. It does not change when you multiply $u$ or $v$ by a positive number. Mathlib uses the same formula for all vectors. With the convention $0 / 0 = 0$, the angle between the zero vector and any vector is then $\pi / 2$.

Explanations

L1 human

Put the two arrows at the same start point. The angle between them is the opening between the arrows, measured in radians from $0$ to $\pi$. For example, $(1, 0)$ and $(0, 1)$ have dot product $0$, so the angle between them is $\arccos 0 = \pi / 2$, a right angle.