mod6_fortyone_prime
plain-language theorem explainer
The declaration establishes that 41 is prime and satisfies the congruence 41 ≡ 5 (mod 6). Number theorists verifying specific residue classes of small primes for arithmetic-function calculations would reference this fact. The proof reduces to a single native_decide call that evaluates both the primality predicate and the modular condition by direct computation.
Claim. $41$ is prime and $41 ≡ 5 (mod 6)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate Prime is the transparent alias Nat.Prime imported from the Basic submodule. This theorem records a concrete numerical instance of a prime lying in the residue class 5 mod 6, a fact that can be used when evaluating arithmetic functions on small primes.
proof idea
The proof is a one-line term that applies native_decide to the conjunction of the primality predicate and the modular equality, letting Lean compute both sides directly from the definitions of Nat.Prime and the remainder operation.
why it matters
It supplies a verified numerical anchor for the prime 41 in the 5 mod 6 class inside the NumberTheory.Primes hierarchy. No downstream theorems currently cite it. The fact sits among other small-prime checks that support later arithmetic-function identities such as Möbius evaluations on square-free integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.