# Documentation

Mathlib.Data.Nat.PrimeFin

# Prime numbers #

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

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

theorem Nat.factors_mul_toFinset {a : } {b : } (ha : a 0) (hb : b 0) :

If a, b are positive, the prime divisors of a * b are the union of those of a and b

theorem Nat.pow_factors_toFinset (n : ) {k : } (hk : k 0) :
theorem Nat.prime_pow_prime_divisor {p : } {k : } (hk : k 0) (hp : ) :

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