English
IsPrimePow n is equivalent to there exists a prime p and exponent k > 0 such that n.factorization = Finsupp.single p k.
Русский
IsPrimePow n эквивалентно существованию простого p и степени k>0, таких что n.factorization = Finsupp.single p k.
LaTeX
$$$IsPrimePow(n) \iff \exists p\ k>0:\ n.factorization = \mathrm{single}(p,k).$$$
Lean4
theorem isPrimePow_iff_factorization_eq_single {n : ℕ} :
IsPrimePow n ↔ ∃ p k : ℕ, 0 < k ∧ n.factorization = Finsupp.single p k :=
by
rw [isPrimePow_nat_iff]
refine exists₂_congr fun p k => ?_
constructor
· rintro ⟨hp, hk, hn⟩
exact ⟨hk, by rw [← hn, Nat.Prime.factorization_pow hp]⟩
· rintro ⟨hk, hn⟩
have hn0 : n ≠ 0 := by
rintro rfl
simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]
exact
⟨Nat.prime_of_mem_primeFactors <| Finsupp.mem_support_iff.2 (by simp [hn, hk.ne'] : n.factorization p ≠ 0), hk,
rfl⟩
