Prime gap

Conjectura.Defs.Mathematics.NumberTheory.PrimeGap

/-
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.Nth
import Mathlib.Data.Nat.Prime.Basic

/-! # Prime gap -/

namespace Conjectura.NumberTheory

/-- The **n-th prime gap** is the distance from the `n`-th prime to the next one. The behaviour
of this sequence — how small it gets infinitely often, how large it can be — is the subject of
much of analytic number theory. -/
noncomputable def primeGap (n : ℕ) : ℕ :=
  Nat.nth Nat.Prime (n + 1) - Nat.nth Nat.Prime n

end Conjectura.NumberTheory