prime_twohundredtwentyseven
plain-language theorem explainer
227 is established as a prime natural number. Number theorists applying arithmetic functions such as the Möbius function to small integers would cite this fact during explicit calculations. The verification reduces to a single native_decide call that performs direct computational primality testing.
Claim. $227$ is a prime number, i.e., its only positive divisors are $1$ and itself.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The Prime predicate is the repo-local alias for Nat.Prime, kept transparent so that standard divisibility facts apply directly. Upstream results supply the basic is-collision-free and is-tautology patterns used elsewhere in the repository, but the present statement relies only on the transparent Prime abbreviation.
proof idea
The proof is a one-line term that applies native_decide to reduce the primality predicate to native computation over the finite set of candidate divisors.
why it matters
The declaration supplies a concrete verified prime inside the NumberTheory.Primes.ArithmeticFunctions component that supports Möbius evaluations and related arithmetic-function identities. It fills a basic fact needed before Dirichlet inversion or square-free checks can be instantiated on explicit integers. No downstream uses are recorded yet, so the result remains a leaf fact awaiting attachment to larger Recognition Science number-theoretic constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.