Prime numbers

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

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

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

instance Nat.Primes.infinite : Infinite Primes

instance Nat.Primes.countable : Countable Primes

def Nat.primeFactors (n : ℕ) : Finset ℕ

The prime factors of a natural number as a finset.

@[simp]

theorem Nat.toFinset_factors (n : ℕ) : n.primeFactorsList.toFinset = n.primeFactors

@[simp]

theorem Nat.mem_primeFactors {n p : ℕ} : p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

theorem Nat.mem_primeFactors_of_ne_zero {n p : ℕ} (hn : n ≠ 0) : p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n

theorem Nat.Prime.mem_primeFactors {n p : ℕ} (hp : Prime p) (hdvd : p ∣ n) (hn : n ≠ 0) : p ∈ n.primeFactors

theorem Nat.Prime.mem_primeFactors' {n p : ℕ} (hp : Prime p) (hdvd : p ∣ n) [NeZero n] : p ∈ n.primeFactors

A version of Nat.Prime.mem_primeFactors using [NeZero n] instead of an explicit argument.

theorem Nat.Prime.mem_primeFactors_self {p : ℕ} (hp : Prime p) : p ∈ p.primeFactors

theorem Nat.primeFactors_mono {m n : ℕ} (hmn : m ∣ n) (hn : n ≠ 0) : m.primeFactors ⊆ n.primeFactors

theorem Nat.mem_primeFactors_iff_mem_primeFactorsList {n p : ℕ} : p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList

theorem Nat.prime_of_mem_primeFactors {n p : ℕ} (hp : p ∈ n.primeFactors) : Prime p

theorem Nat.dvd_of_mem_primeFactors {n p : ℕ} (hp : p ∈ n.primeFactors) : p ∣ n

theorem Nat.pos_of_mem_primeFactors {n p : ℕ} (hp : p ∈ n.primeFactors) : 0 < p

theorem Nat.le_of_mem_primeFactors {n p : ℕ} (h : p ∈ n.primeFactors) : p ≤ n

@[simp]

theorem Nat.primeFactors_zero : primeFactors 0 = ∅

@[simp]

theorem Nat.primeFactors_one : primeFactors 1 = ∅

@[simp]

theorem Nat.primeFactors_eq_empty {n : ℕ} : n.primeFactors = ∅ ↔ n = 0 ∨ n = 1

@[simp]

theorem Nat.nonempty_primeFactors {n : ℕ} : n.primeFactors.Nonempty ↔ 1 < n

@[simp]

theorem Nat.Prime.primeFactors {p : ℕ} (hp : Prime p) : p.primeFactors = {p}

theorem Nat.primeFactors_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (a * b).primeFactors = a.primeFactors ∪ b.primeFactors

theorem Nat.Coprime.primeFactors_mul {a b : ℕ} (hab : a.Coprime b) : (a * b).primeFactors = a.primeFactors ∪ b.primeFactors

theorem Nat.primeFactors_gcd {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors

@[simp]

theorem Nat.disjoint_primeFactors {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : Disjoint a.primeFactors b.primeFactors ↔ a.Coprime b

theorem Nat.Coprime.disjoint_primeFactors {a b : ℕ} (hab : a.Coprime b) : Disjoint a.primeFactors b.primeFactors

theorem Nat.primeFactors_pow_succ (n k : ℕ) : (n ^ (k + 1)).primeFactors = n.primeFactors

theorem Nat.primeFactors_pow {k : ℕ} (n : ℕ) (hk : k ≠ 0) : (n ^ k).primeFactors = n.primeFactors

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