# Prime numbers #

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

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

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

Equations
Equations
def Nat.primeFactors (n : ) :

The prime factors of a natural number as a finset.

Equations
• n.primeFactors = n.factors.toFinset
Instances For
@[simp]
theorem Nat.toFinset_factors (n : ) :
n.factors.toFinset = n.primeFactors
@[simp]
theorem Nat.mem_primeFactors {n : } {p : } :
p n.primeFactors p.Prime p n n 0
theorem Nat.mem_primeFactors_of_ne_zero {n : } {p : } (hn : n 0) :
p n.primeFactors p.Prime p n
theorem Nat.primeFactors_mono {m : } {n : } (hmn : m n) (hn : n 0) :
m.primeFactors n.primeFactors
theorem Nat.mem_primeFactors_iff_mem_factors {n : } {p : } :
p n.primeFactors p n.factors
theorem Nat.prime_of_mem_primeFactors {n : } {p : } (hp : p n.primeFactors) :
p.Prime
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]
@[simp]
@[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 : p.Prime) :
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 : p.Prime) :
(p ^ k).primeFactors = {p}

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