mod6_sixtyone_prime
plain-language theorem explainer
61 is prime and satisfies 61 ≡ 1 mod 6. Number theorists verifying splitting laws or quadratic reciprocity in extensions tied to the modulus 6 would cite this basic arithmetic fact. The verification is a one-line native decision that evaluates both primality and the remainder by direct computation.
Claim. $61$ is a prime number and $61 ≡ 1 (mod 6)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard notion of primality on natural numbers. This theorem records a concrete instance of a prime in the residue class 1 mod 6, placed among sibling facts on squarefree numbers and Möbius values.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the conjunction of primality and the modular arithmetic condition by direct computation.
why it matters
This supplies a concrete prime in the 1 mod 6 class for use in arithmetic-function identities. It depends only on the local definition of Prime and fills a basic slot in the primes hierarchy without invoking deeper Dirichlet algebra. No downstream applications are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.