mod6_eightythree_prime
plain-language theorem explainer
The declaration asserts that 83 is prime and congruent to 5 modulo 6. Number theorists applying arithmetic functions such as the Möbius function to primes in residue class 5 mod 6 would cite this concrete check. The proof is a one-line native decision procedure that evaluates the conjunction directly.
Claim. $83$ is prime and $83 ≡ 5 mod 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the local transparent alias for the standard predicate Nat.Prime on natural numbers. This supplies a specific numerical instance of a prime in the 5 mod 6 class that can support later squarefree or inversion calculations.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the conjunction of primality and the modular equality.
why it matters
The result supplies a concrete numerical fact inside the arithmetic-functions module that can feed Möbius applications to primes in the 5 mod 6 class. It sits downstream of the Basic.Prime alias and has no recorded downstream uses. No open questions or Recognition Science landmarks are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.