mod6_thirtyone_prime
plain-language theorem explainer
31 is established as prime and congruent to 1 modulo 6. Number theorists working on modular conditions for small primes in the Recognition Science arithmetic functions module would cite this fact when checking residue classes. The verification proceeds via a single native decision procedure that confirms both primality and the modular equality directly.
Claim. $31$ is prime and $31 ≡ 1$ (mod $6$).
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. This theorem supplies a basic modular fact about the prime 31. It depends on the transparent alias Prime, defined as the standard notion of primality for natural numbers.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of primality and the residue condition.
why it matters
This supplies a concrete instance of a prime in the residue class 1 mod 6, supporting modular properties within the arithmetic functions section. It provides a building block for prime-related checks in the module, though no downstream theorems are recorded. It touches on number theory foundations without direct linkage to chain steps such as T5 J-uniqueness or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.