Prime powers and factorizations

This file deals with factorizations of prime powers.

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

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

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

theorem isPrimePow_iff_factorization_eq_single {n : ℕ} : IsPrimePow n ↔ ∃ p k, 0 < k ∧ Nat.factorization n = fun₀ | p => k

theorem isPrimePow_iff_card_support_factorization_eq_one {n : ℕ} : IsPrimePow n ↔ Finset.card (Nat.factorization n).support = 1

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

theorem exists_ord_compl_eq_one_iff_isPrimePow {n : ℕ} (hn : n ≠ 1) : IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) 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 : Nat.Coprime a b) (hn : IsPrimePow n) : n ∣ a * b ↔ n ∣ a ∨ n ∣ b

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