HepLean Documentation

Mathlib.Data.Nat.Factorization.PrimePow

Prime powers and factorizations #

This file deals with factorizations of prime powers.

source
theorem IsPrimePow.minFac_pow_factorization_eq {n : ℕ} (hn : IsPrimePow n) :
n.minFac ^ n.factorization n.minFac = n
source
theorem isPrimePow_of_minFac_pow_factorization_eq {n : ℕ} (h : n.minFac ^ n.factorization n.minFac = n) (hn : n ≠ 1) :
IsPrimePow n
source
theorem isPrimePow_iff_minFac_pow_factorization_eq {n : ℕ} (hn : n ≠ 1) :
IsPrimePow n ↔ n.minFac ^ n.factorization n.minFac = n
source
theorem isPrimePow_iff_factorization_eq_single {n : ℕ} :
IsPrimePow n ↔ ∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k
source
theorem isPrimePow_iff_card_primeFactors_eq_one {n : ℕ} :
IsPrimePow n ↔ n.primeFactors.card = 1
source
theorem IsPrimePow.exists_ordCompl_eq_one {n : ℕ} (h : IsPrimePow n) :
∃ (p : ℕ), Nat.Prime p ∧ n / p ^ n.factorization p = 1
source
@[deprecated IsPrimePow.exists_ordCompl_eq_one]
theorem IsPrimePow.exists_ord_compl_eq_one {n : ℕ} (h : IsPrimePow n) :
∃ (p : ℕ), Nat.Prime p ∧ n / p ^ n.factorization p = 1

Alias of IsPrimePow.exists_ordCompl_eq_one.

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

Alias of exists_ordCompl_eq_one_iff_isPrimePow.

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

source
theorem isPrimePow_pow_iff {n k : ℕ} (hk : k ≠ 0) :
IsPrimePow (n ^ k) ↔ IsPrimePow n
source
theorem Nat.Coprime.isPrimePow_dvd_mul {n a b : ℕ} (hab : a.Coprime b) (hn : IsPrimePow n) :
n ∣ a * b ↔ n ∣ a ∨ n ∣ b
source
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)
source
theorem IsPrimePow.factorization_minFac_ne_zero {n : ℕ} (hn : IsPrimePow n) :
n.factorization n.minFac ≠ 0
source
def Nat.Primes.prodNatEquiv :
Nat.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.
Instances For
    source
    @[simp]
    theorem Nat.Primes.prodNatEquiv_apply (p : Nat.Primes) (k : ℕ) :
    Nat.Primes.prodNatEquiv (p, k) = ⟨↑p ^ (k + 1), ⋯⟩
    source
    @[simp]
    theorem Nat.Primes.coe_prodNatEquiv_apply (p : Nat.Primes) (k : ℕ) :
    ↑(Nat.Primes.prodNatEquiv (p, k)) = ↑p ^ (k + 1)
    source
    @[simp]
    theorem Nat.Primes.prodNatEquiv_symm_apply {n : ℕ} (hn : IsPrimePow n) :
    Nat.Primes.prodNatEquiv.symm ⟨n, hn⟩ = (⟨n.minFac, ⋯⟩, n.factorization n.minFac - 1)