Infinitely Many Primes
Open
Theorem
1
2
-- There are infinitely many prime numbers. theorem inf_primes : ∀ n : ℕ, ∃ p : ℕ, n < p ∧ Nat.Prime p :=
-- There are infinitely many prime numbers. theorem inf_primes : ∀ n : ℕ, ∃ p : ℕ, n < p ∧ Nat.Prime p :=