English
IsPrimePow n iff there exists a unique prime p with p ∣ n and p is prime.
Русский
IsPrimePow n эквивалентно существованию единственного простого p, делящего n.
LaTeX
$$$IsPrimePow(n) \iff \exists! p:\mathbb{N}, p.Prime \land p \mid n.$$$
Lean4
/-- An equivalent definition for prime powers: `n` is a prime power iff there is a unique prime
dividing it. -/
theorem isPrimePow_iff_unique_prime_dvd {n : ℕ} : IsPrimePow n ↔ ∃! p : ℕ, p.Prime ∧ p ∣ n :=
by
rw [isPrimePow_nat_iff]
constructor
· rintro ⟨p, k, hp, hk, rfl⟩
refine ⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, ?_⟩
rintro q ⟨hq, hq'⟩
exact (Nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq')
rintro ⟨p, ⟨hp, hn⟩, hq⟩
rcases eq_or_ne n 0 with (rfl | hn₀)
· cases (hq 2 ⟨Nat.prime_two, dvd_zero 2⟩).trans (hq 3 ⟨Nat.prime_three, dvd_zero 3⟩).symm
refine ⟨p, n.factorization p, hp, hp.factorization_pos_of_dvd hn₀ hn, ?_⟩
simp only [and_imp] at hq
apply
Nat.dvd_antisymm
(Nat.ordProj_dvd _ _)
-- We need to show n ∣ p ^ n.factorization p
apply Nat.dvd_of_primeFactorsList_subperm hn₀
rw [hp.primeFactorsList_pow, List.subperm_ext_iff]
intro q hq'
rw [Nat.mem_primeFactorsList hn₀] at hq'
cases hq _ hq'.1 hq'.2
simp
