Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Admissible tuple

IsAdmissibledef

A finite set of shifts is admissible when, for every prime p, the shifts miss at least one residue class mod p. Inadmissible tuples are blocked from being prime infinitely often for a trivial congruence reason, so admissibility is exactly the hypothesis under which the Hardy–Littlewood conjectures are stated.

def IsAdmissible (H : Finset ℕ) : Prop :=
  ∀ p : ℕ, p.Prime → ∃ r : ZMod p, ∀ h ∈ H, (h : ZMod p) ≠ r

Used by

From Mathlib

import Conjectura.Defs.Mathematics.NumberTheory.AdmissibleTuple · maintainer — open · raw source

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

Full credits