prime_twohundredeightyone
plain-language theorem explainer
281 is established as a prime natural number. Researchers applying arithmetic functions such as the Möbius function to specific integers would cite this result to confirm that 281 contributes to sums without square factors. The proof is a direct computational verification via native_decide.
Claim. $281$ is a prime number, i.e., the predicate that $n$ is a prime natural number holds at $n=281$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime. The local setting keeps statements minimal so that deeper Dirichlet inversion can be added once basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that invokes native_decide to computationally verify the primality of 281.
why it matters
This supplies a concrete primality fact inside the arithmetic-functions module that supports Möbius and big-Omega calculations on 281. It fills a basic check required by the NumberTheory.Primes section without touching the forcing chain or RS constants. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.