Documentation

Mathlib.Data.Nat.PrimeFin

Prime numbers #

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

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

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

The prime factors of a natural number as a finset.

Equations
  • n.primeFactors = n.primeFactorsList.toFinset
Instances For
    @[simp]
    theorem Nat.toFinset_factors (n : ) :
    n.primeFactorsList.toFinset = n.primeFactors
    @[simp]
    theorem Nat.mem_primeFactors {n : } {p : } :
    p n.primeFactors Nat.Prime p p n n 0
    theorem Nat.mem_primeFactors_of_ne_zero {n : } {p : } (hn : n 0) :
    p n.primeFactors Nat.Prime p p n
    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
    @[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.

    theorem Nat.prime_of_mem_primeFactors {n : } {p : } (hp : p n.primeFactors) :
    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_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 : Nat.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 : Nat.Prime p) :
    (p ^ k).primeFactors = {p}

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