mod6_onehundredthree_prime
plain-language theorem explainer
103 is prime and congruent to 1 modulo 6. Number theorists checking small-prime residues for arithmetic-function identities would cite the result as a verified instance. The proof is a one-line native_decide wrapper that evaluates both conjuncts by direct computation.
Claim. $103$ is prime and $103 ≡ 1 mod 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting is the preparation of basic number-theoretic tools for later Dirichlet-algebra layers. The sole upstream dependency is the transparent alias Prime for Nat.Prime.
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
The declaration supplies a concrete modular fact marked RS-relevant for 103. It sits among the arithmetic-function footholds but has no recorded downstream uses in the current graph. The result therefore functions as a ready-to-hand instance rather than a lemma feeding a larger theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.