Prime powers and factorizations

This file deals with factorizations of prime powers.

theorem IsPrimePow.minFac_pow_factorization_eq {n : ℕ} (hn : IsPrimePow n) : n.minFac ^ n.factorization n.minFac = n

theorem isPrimePow_of_minFac_pow_factorization_eq {n : ℕ} (h : n.minFac ^ n.factorization n.minFac = n) (hn : n ≠ 1) : IsPrimePow n

theorem isPrimePow_iff_minFac_pow_factorization_eq {n : ℕ} (hn : n ≠ 1) : IsPrimePow n ↔ n.minFac ^ n.factorization n.minFac = n

theorem isPrimePow_iff_factorization_eq_single {n : ℕ} : IsPrimePow n ↔ ∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k

theorem isPrimePow_iff_card_primeFactors_eq_one {n : ℕ} : IsPrimePow n ↔ n.primeFactors.card = 1

theorem IsPrimePow.exists_ord_compl_eq_one {n : ℕ} (h : IsPrimePow n) : ∃ (p : ℕ), Nat.Prime p ∧ n / p ^ n.factorization p = 1

theorem exists_ord_compl_eq_one_iff_isPrimePow {n : ℕ} (hn : n ≠ 1) : IsPrimePow n ↔ ∃ (p : ℕ), Nat.Prime p ∧ n / p ^ n.factorization p = 1

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

An equivalent definition for prime powers: n is a prime power iff there is a unique prime dividing it.

theorem isPrimePow_pow_iff {n : ℕ} {k : ℕ} (hk : k ≠ 0) : IsPrimePow (n ^ k) ↔ IsPrimePow n

theorem Nat.Coprime.isPrimePow_dvd_mul {n : ℕ} {a : ℕ} {b : ℕ} (hab : a.Coprime b) (hn : IsPrimePow n) : n ∣ a * b ↔ n ∣ a ∨ n ∣ b

theorem Nat.mul_divisors_filter_prime_pow {a : ℕ} {b : ℕ} (hab : a.Coprime b) : Finset.filter IsPrimePow (a * b).divisors = Finset.filter IsPrimePow (a.divisors ∪ b.divisors)