English
A number n is a prime power iff there exists a prime p and k≥0 with n = p^(k+1).
Русский
Число n является степенью простого p тогда и только тогда, когда существует p и k≥0 такое, что n = p^(k+1).
LaTeX
$$$\text{IsPrimePow } n \;\Longleftrightarrow\; \exists p\;\exists k\; (\text{Prime } p) \land p^{(k+1)} = n$$$
Lean4
/-- An equivalent definition for prime powers: `n` is a prime power iff there is a prime `p` and a
natural `k` such that `n` can be written as `p^(k+1)`. -/
theorem isPrimePow_iff_pow_succ : IsPrimePow n ↔ ∃ (p : R) (k : ℕ), Prime p ∧ p ^ (k + 1) = n :=
(isPrimePow_def _).trans
⟨fun ⟨p, k, hp, hk, hn⟩ => ⟨p, k - 1, hp, by rwa [Nat.sub_add_cancel hk]⟩, fun ⟨_, _, hp, hn⟩ =>
⟨_, _, hp, Nat.succ_pos', hn⟩⟩
