Euclids_Theorem

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

euclid-s-theoremprime-numbersproofwiki

For any finite set of prime numbers, there exists a prime number not in that set.

Preamble

import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Tactic

Formal statement

theorem Euclids_Theorem (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : ∃ q, Nat.Prime q ∧ q ∉ S := by sorry

Source