prime_fourhundredsixtyseven
plain-language theorem explainer
467 is asserted to be a prime natural number. Number theorists applying the Möbius function or square-free checks in the Recognition Science arithmetic layer would reference this fact when 467 divides an argument. The proof is a one-line computational discharge via the native_decide tactic.
Claim. $467$ is a prime number, i.e., the predicate Prime holds at 467 where Prime is the standard primality predicate on natural numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repo-local transparent alias for the standard primality predicate on natural numbers. The local setting is a collection of basic footholds for Dirichlet algebra and inversion once the interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the primality goal by direct computation.
why it matters
The declaration supplies a concrete prime fact inside the arithmetic-functions file. It supports Möbius-function applications in the NumberTheory.Primes layer of the Recognition Science framework. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.