Infinitude of primes

Conjectura.Statements.Mathematics.NumberTheory.InfinitelyManyPrimes

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.Data.Nat.Prime.Infinite

/-! # Infinitude of primes -/

namespace Conjectura.NumberTheory

/-- **Infinitely many primes**: for every bound there is a prime beyond it. Euclid's theorem;
present here as the smallest non-trivial statement in the corpus, useful as a worked example. -/
def InfinitelyManyPrimes : Prop := ∀ N : ℕ, ∃ p : ℕ, N ≤ p ∧ p.Prime

end Conjectura.NumberTheory