Euler's totient function

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$.