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 = fun₀ | p => k

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

theorem Nat.not_isPrimePow_iff_nontrivial_of_two_le {n : ℕ} (hn : 2 ≤ n) : ¬IsPrimePow n ↔ n.primeFactors.Nontrivial

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

theorem exists_ordCompl_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) : {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}

def Nat.Primes.prodNatEquiv : Primes × ℕ ≃ { n : ℕ // IsPrimePow n }

The canonical equivalence between pairs (p, k) with p a prime and k : ℕ and the set of prime powers given by (p, k) ↦ p^(k+1).

@[simp]

theorem Nat.Primes.prodNatEquiv_apply (p : Primes) (k : ℕ) : prodNatEquiv (p, k) = ⟨↑p ^ (k + 1), ⋯⟩

@[simp]

theorem Nat.Primes.coe_prodNatEquiv_apply (p : Primes) (k : ℕ) : ↑(prodNatEquiv (p, k)) = ↑p ^ (k + 1)

@[simp]

theorem Nat.Primes.prodNatEquiv_symm_apply {n : ℕ} (hn : IsPrimePow n) : prodNatEquiv.symm ⟨n, hn⟩ = (⟨n.minFac, ⋯⟩, n.factorization n.minFac - 1)

theorem Nat.exponent_eq_exponent_mul_factorization_of_prime_pow_eq_base_pow {p a m n : ℕ} (hp : Prime p) (h : p ^ m = a ^ n) : m = n * a.factorization p

theorem Nat.exponent_dvd_of_prime_pow_eq_pow {p a m n : ℕ} (hp : Prime p) (h : p ^ m = a ^ n) : n ∣ m

theorem Nat.exists_base_eq_prime_pow_of_prime_pow_eq_base_pow {p a m n : ℕ} (hp : Prime p) (hn : n ≠ 0) (h : p ^ m = a ^ n) : ∃ (k : ℕ), a = p ^ k