Values of Euler\'s function: $\varphi(17)$, $\varphi(p)$, $\varphi(p^2)$, $\varphi(p^\alpha)$

This is Problem 4.132 of N. B. Alfutova and A. V. Ustinov, Algebra and Number Theory (MCCME, 2002), Chapter 4, §4 “Theorems of Fermat and Euler”.

Euler's function $\varphi(n)$ is the number of integers among $1,2,\dots,n$ that are coprime to $n$. The problem asks for (a) $\varphi(17)$, (b) $\varphi(p)$, (c) $\varphi(p^2)$, (d) $\varphi(p^{\alpha})$, where $p$ is a prime and $\alpha\ge 1$ is a natural number.

Theorem. For every prime $p$ and every integer $\alpha\ge1$:

1. $\varphi(17)=16$;
2. $\varphi(p)=p-1$;
3. $\varphi(p^{2})=p(p-1)$;

These values, together with multiplicativity, give the standard product formula for Euler's function.

Formalization Note Euler's function is Mathlib's Nat.totient, which counts the $k\in\{0,\dots,n-1\}$ with $\gcd(k,n)=1$; for $n\ge1$ this agrees with the book's definition. The subtractions $p-1$ and $\alpha-1$ are natural-number subtractions, exact because $p\ge 2$ and $\alpha\ge 1$.