prime_onehundredthirtyone
plain-language theorem explainer
131 is shown to be prime. Workers with arithmetic functions on small primes cite this when needed. The proof uses native_decide for direct verification.
Claim. $131$ is a prime number.
background
The module wraps Mathlib arithmetic functions, starting with the Möbius function. Prime is a transparent alias for the standard Nat.Prime predicate on natural numbers. This supplies the concrete case for 131 ahead of deeper Dirichlet algebra.
proof idea
One-line wrapper applying the native_decide tactic to the primality predicate.
why it matters
Supplies a basic primality fact inside the arithmetic functions module. No downstream uses are recorded. It supports later Möbius and squarefree calculations within the number theory layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.