# Prime numbers #

This file contains some results about prime numbers which depend on finiteness of sets.

source
theorem Nat.infinite_setOf_prime :
{p : ℕ | Prime p}.Infinite

A version of `Nat.exists_infinite_primes` using the `Set.Infinite` predicate.

source
instance Nat.Primes.infinite :
Infinite Primes
source
instance Nat.Primes.countable :
Countable Primes
source
def Nat.primeFactors (n : ℕ) :
Finset ℕ

The prime factors of a natural number as a finset.

Equations

- n.primeFactors = n.primeFactorsList.toFinset

Instances For

source
@[simp]
theorem Nat.toFinset_factors (n : ℕ) :
n.primeFactorsList.toFinset = n.primeFactors
source
@[simp]
theorem Nat.mem_primeFactors {n p : ℕ} :
p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
source
theorem Nat.mem_primeFactors_of_ne_zero {n p : ℕ} (hn : n ≠ 0) :
p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n
source
theorem Nat.primeFactors_mono {m n : ℕ} (hmn : m ∣ n) (hn : n ≠ 0) :
m.primeFactors ⊆ n.primeFactors
source
theorem Nat.mem_primeFactors_iff_mem_primeFactorsList {n p : ℕ} :
p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList
source
theorem Nat.prime_of_mem_primeFactors {n p : ℕ} (hp : p ∈ n.primeFactors) :
Prime p
source
theorem Nat.dvd_of_mem_primeFactors {n p : ℕ} (hp : p ∈ n.primeFactors) :
p ∣ n
source
theorem Nat.pos_of_mem_primeFactors {n p : ℕ} (hp : p ∈ n.primeFactors) :
0 < p
source
theorem Nat.le_of_mem_primeFactors {n p : ℕ} (h : p ∈ n.primeFactors) :
p ≤ n
source
@[simp]
theorem Nat.primeFactors_zero :
primeFactors 0 = ∅
source
@[simp]
theorem Nat.primeFactors_one :
primeFactors 1 = ∅
source
@[simp]
theorem Nat.primeFactors_eq_empty {n : ℕ} :
n.primeFactors = ∅ ↔ n = 0 ∨ n = 1
source
@[simp]
theorem Nat.nonempty_primeFactors {n : ℕ} :
n.primeFactors.Nonempty ↔ 1 < n
source
@[simp]
theorem Nat.Prime.primeFactors {p : ℕ} (hp : Prime p) :
p.primeFactors = {p}
source
theorem Nat.primeFactors_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
(a * b).primeFactors = a.primeFactors ∪ b.primeFactors
source
theorem Nat.Coprime.primeFactors_mul {a b : ℕ} (hab : a.Coprime b) :
(a * b).primeFactors = a.primeFactors ∪ b.primeFactors
source
theorem Nat.primeFactors_gcd {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
(a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors
source
@[simp]
theorem Nat.disjoint_primeFactors {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
Disjoint a.primeFactors b.primeFactors ↔ a.Coprime b
source
theorem Nat.Coprime.disjoint_primeFactors {a b : ℕ} (hab : a.Coprime b) :
Disjoint a.primeFactors b.primeFactors
source
theorem Nat.primeFactors_pow_succ (n k : ℕ) :
(n ^ (k + 1)).primeFactors = n.primeFactors
source
theorem Nat.primeFactors_pow {k : ℕ} (n : ℕ) (hk : k ≠ 0) :
(n ^ k).primeFactors = n.primeFactors
source
theorem Nat.primeFactors_prime_pow {k p : ℕ} (hk : k ≠ 0) (hp : Prime p) :
(p ^ k).primeFactors = {p}

The only prime divisor of positive prime power `p^k` is `p` itself