mathlib3 documentation

data.nat.prime_fin

Prime numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_to_finset {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_to_finset (n : ) {k : } (hk : k 0) :
theorem nat.prime_pow_prime_divisor {p k : } (hk : k 0) (hp : nat.prime p) :
(p ^ k).factors.to_finset = {p}

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