Documentation

Mathlib.Data.Nat.PrimeFin

Prime numbers #

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

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

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

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

The prime factors of a natural number as a finset.

Equations
  • n.primeFactors = n.primeFactorsList.toFinset
source
@[simp]
theorem Nat.toFinset_factors (n : ℕ) :
n.primeFactorsList.toFinset = n.primeFactors
source
@[simp]
theorem Nat.mem_primeFactors {n : ℕ} {p : ℕ} :
p ∈ n.primeFactors ↔ Nat.Prime p ∧ p ∣ n ∧ n ≠ 0
source
theorem Nat.mem_primeFactors_of_ne_zero {n : ℕ} {p : ℕ} (hn : n ≠ 0) :
p ∈ n.primeFactors ↔ Nat.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
@[deprecated Nat.mem_primeFactors_iff_mem_primeFactorsList]
theorem Nat.mem_primeFactors_iff_mem_factors {n : ℕ} {p : ℕ} :
p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList

Alias of Nat.mem_primeFactors_iff_mem_primeFactorsList.

source
theorem Nat.prime_of_mem_primeFactors {n : ℕ} {p : ℕ} (hp : p ∈ n.primeFactors) :
Nat.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 :
Nat.primeFactors 0 = ∅
source
@[simp]
theorem Nat.primeFactors_one :
Nat.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 : Nat.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 : Nat.Prime p) :
(p ^ k).primeFactors = {p}

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