Euler's totient function

Definition

Let $n$ be a positive integer. Euler's totient function $\varphi(n)$ is the number of integers $k$ with $1 \le k \le n$ such that $k$ and $n$ are coprime.

Remarks

For example, $\varphi(1) = 1$, $\varphi(9) = 6$ and $\varphi(12) = 4$. The integers coprime to $12$ in $\{1, \dots, 12\}$ are $1, 5, 7, 11$. The number $\varphi(n)$ is the number of elements of a reduced residue system modulo $n$. If $n = p_1^{e_1} \cdots p_r^{e_r}$ with distinct primes $p_i$, then $\varphi(n) = n \prod_{i=1}^{r} \left(1 - \frac{1}{p_i}\right)$. The Lean library Mathlib sets $\varphi(0) = 0$.

Explanations

L1 human

Count the numbers from $1$ to $n$ that have no common factor with $n$. For $n = 10$, these are $1, 3, 7, 9$, so $\varphi(10) = 4$.