prime_quadruplet_eleven
plain-language theorem explainer
Eleven, thirteen, seventeen, and nineteen form a prime quadruplet with successive gaps 2, 4, and 2. Number theorists working with explicit prime constellations or preparing arithmetic-function examples would cite this instance. The proof reduces to a single native_decide invocation that computationally confirms all four primality claims.
Claim. The integers $11$, $13$, $17$, and $19$ are each prime and satisfy the quadruplet condition with differences $2$, $4$, and $2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream results include basic primality definitions together with assorted foundational structures whose doc-comments describe algebraic tautologies or collision-free classes.
proof idea
One-line wrapper that applies native_decide to the conjunction of four primality assertions.
why it matters
The statement supplies a concrete prime quadruplet inside the arithmetic-functions module. No downstream theorems are recorded. It contributes a basic number-theoretic fact that can support later Möbius or square-free applications without engaging the forcing chain, RCL, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.