An odd perfect number is not a perfect square

Corollary of Euler's form. No odd perfect number is a perfect square. Concretely, if $N$ is odd and $\sigma(N) = 2N$, then there is no $r$ with $N = r^2$.

One route is through Euler's form $N = p^k m^2$ with $k \equiv 1 \pmod 4$: the exponent of the special prime $p$ is odd, so $N$ cannot be a square. A second, self-contained route uses the parity of $\sigma$: for odd $N$, $\sigma(N)$ is odd precisely when $N$ is a square, whereas $\sigma(N) = 2N$ is even.

Formalized with Mathlib's IsSquare predicate on ℕ.