mod6_thirteen_prime
plain-language theorem explainer
13 is prime and satisfies 13 ≡ 1 mod 6. Elementary number theorists verifying small cases for Dirichlet progressions or Möbius inversion on squarefree integers cite this fact. The proof applies the native_decide tactic to evaluate the conjunction of primality and the modular condition in one computational step.
Claim. The integer 13 is prime and satisfies the congruence $13 ≡ 1 mod 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is defined locally as a transparent alias for the standard primality predicate on natural numbers. The declaration depends on the upstream abbrev Prime (n : ℕ) : Prop := Nat.Prime n from the Basic module.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute both the primality of 13 and the remainder 13 % 6 directly.
why it matters
This supplies a verified small-prime fact inside the arithmetic-functions module that supports Möbius-based arguments. It has no listed downstream uses. The result fills a basic number-theoretic placeholder without engaging the core forcing chain, J-uniqueness, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.