mod6_nineteen_prime
plain-language theorem explainer
19 is prime and congruent to 1 modulo 6. Researchers working with arithmetic functions on primes in specific residue classes would cite this fact when verifying modular conditions for small cases. The proof reduces to a single native_decide invocation that evaluates the conjunction by direct computation.
Claim. $19$ is prime and $19$ is congruent to $1$ modulo $6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is introduced in the sibling Basic module as a transparent alias for the standard Nat.Prime predicate on natural numbers. This theorem depends only on that alias to assert both primality of 19 and the stated congruence.
proof idea
The proof is a one-line term-mode wrapper that applies the native_decide tactic directly to the conjunction, confirming both components through computational evaluation.
why it matters
This supplies a verified concrete instance of a prime in the residue class 1 mod 6 inside the arithmetic functions module. No downstream uses are recorded, so it functions as a basic fact that may later support residue-class checks in Dirichlet algebra or Möbius inversion layers. It aligns with the module's focus on lightweight interfaces rather than deep chain steps in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.