Prime numbers

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

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

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

instance Nat.Primes.infinite : Infinite Nat.Primes

Equations

• Nat.Primes.infinite = Nat.Primes.infinite.proof_1

instance Nat.Primes.countable : Countable Nat.Primes

Equations

• Nat.Primes.countable = Nat.Primes.countable.proof_1

theorem Nat.factors_mul_toFinset {a : ℕ} {b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : List.toFinset (Nat.factors (a * b)) = List.toFinset (Nat.factors a) ∪ List.toFinset (Nat.factors b)

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

theorem Nat.pow_succ_factors_toFinset (n : ℕ) (k : ℕ) : List.toFinset (Nat.factors (n ^ (k + 1))) = List.toFinset (Nat.factors n)

theorem Nat.pow_factors_toFinset (n : ℕ) {k : ℕ} (hk : k ≠ 0) : List.toFinset (Nat.factors (n ^ k)) = List.toFinset (Nat.factors n)

theorem Nat.prime_pow_prime_divisor {p : ℕ} {k : ℕ} (hk : k ≠ 0) (hp : Nat.Prime p) : List.toFinset (Nat.factors (p ^ k)) = {p}

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

theorem Nat.factors_mul_toFinset_of_coprime {a : ℕ} {b : ℕ} (hab : Nat.Coprime a b) : List.toFinset (Nat.factors (a * b)) = List.toFinset (Nat.factors a) ∪ List.toFinset (Nat.factors b)