isPrimePow_iff_unique_prime_dvd

theorem isPrimePow_iff_unique_prime_dvd : ∀ {n : ℕ}, IsPrimePow n ↔ ∃! p, p.Prime ∧ p ∣ n

The theorem `isPrimePow_iff_unique_prime_dvd` provides an equivalent definition for prime powers. It states that a natural number `n` is a prime power if and only if there exists a unique prime number `p` that divides `n`. In other words, `n` is a prime power exactly when there is one and only one prime number that can divide `n` without leaving a remainder.

More concisely: A natural number `n` is a prime power if and only if there exists a unique prime number `p` such that `p^k = n` for some `k`.