Prime numbers #

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

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

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

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