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 : ℕ | 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
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