prime_onehundredeightyone
plain-language theorem explainer
The declaration establishes that 181 is a prime number. Number theorists working with arithmetic functions in the Recognition Science context would reference this fact when verifying properties of the Möbius function or square-free integers involving 181. The proof proceeds via a direct computational decision procedure that confirms primality without manual factorization steps.
Claim. The natural number $181$ satisfies the primality predicate.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The primality predicate is the repo-local alias for the standard natural-number primality check. This result depends on the basic definition of primality imported from the primes module.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to computationally verify the primality of 181.
why it matters
This fact supplies a concrete prime instance needed for arithmetic-function statements such as Möbius evaluations on square-free inputs. It occupies a basic slot in the number-theory layer of the Recognition Science foundations, though no downstream theorems yet cite it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.