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.

source
theorem nat.infinite_set_of_prime  :
{p : ℕ | nat.prime p}.infinite

A version of nat.exists_infinite_primes using the set.infinite predicate.

source
theorem nat.factors_mul_to_finset {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
(a * b).factors.to_finset = a.factors.to_finset ∪ b.factors.to_finset

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

source
theorem nat.pow_succ_factors_to_finset (n k : ℕ) :
(n ^ (k + 1)).factors.to_finset = n.factors.to_finset
source
theorem nat.pow_factors_to_finset (n : ℕ) {k : ℕ} (hk : k ≠ 0) :
(n ^ k).factors.to_finset = n.factors.to_finset
source
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

source
theorem nat.factors_mul_to_finset_of_coprime {a b : ℕ} (hab : a.coprime b) :
(a * b).factors.to_finset = a.factors.to_finset ∪ b.factors.to_finset