mod6_thirtyseven_prime
plain-language theorem explainer
37 is prime and congruent to 1 modulo 6. Number theorists building arithmetic functions around the Möbius function would cite this explicit residue-class fact. The proof reduces to a single native_decide call that evaluates both conditions directly.
Claim. 37 is prime and $37 ≡ 1 mod 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ for later Dirichlet inversion work. The local setting keeps statements minimal until the basic interfaces stabilize. The sole upstream dependency is the transparent alias Prime for the standard primality predicate on natural numbers.
proof idea
Term-mode proof consisting of one native_decide tactic that checks the conjunction of primality and the modular condition at compile time.
why it matters
The declaration supplies a concrete RS-relevant instance of a prime in the 1 mod 6 class. No downstream theorems are recorded, so it functions as a base fact available for arithmetic-function constructions. It aligns with the module's role of providing explicit number-theoretic footholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.