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_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}

@[deprecated Nat.factorization_minFac_ne_zero (since := "2025-07-21")]

theorem IsPrimePow.factorization_minFac_ne_zero {n : ℕ} (hn : IsPrimePow n) : n.factorization n.minFac ≠ 0

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).

Equations

• One or more equations did not get rendered due to their size.

@[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)