Euler's form of an odd perfect number

Euler's theorem on odd perfect numbers (1849). Suppose $N$ is an odd perfect number, i.e. $N$ is odd and $\sigma(N) = 2N$, where $\sigma$ is the sum-of-divisors function. Then $N$ has the shape

where $p$ is a prime with $p \equiv 1 \pmod 4$, the exponent satisfies $k \equiv 1 \pmod 4$, and $p \nmid m$. The prime power $p^{k}$ is called the special (or Euler) component of $N$; the remaining part $m^2$ is a square, and it is coprime to $p$.

The statement is formalized for natural numbers, with perfection given by Mathlib's Nat.Perfect (which includes positivity) and the congruences written as p % 4 = 1 and k % 4 = 1. Note that $m$ is automatically odd, since $N$ is.