prime_fourhundredeightyseven
plain-language theorem explainer
487 is a prime number. Number theorists building arithmetic functions in the Recognition Science library would cite this when checking Möbius values or square-free properties at this specific integer. The proof is a one-line term that invokes native_decide to settle the decidable primality predicate by direct computation.
Claim. $487$ is prime, i.e., $487$ satisfies the predicate $Nat.Prime(487)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime. The local setting is a collection of small, stable interfaces that later support Dirichlet inversion and related algebra; no deeper analytic number theory is attempted here.
proof idea
One-line term proof that applies native_decide to the decidable proposition Prime 487.
why it matters
The declaration supplies a concrete prime fact inside the ArithmeticFunctions module. It supports downstream use of Möbius and related functions at 487, consistent with the module's goal of providing stable footholds before layering Dirichlet algebra. No parent theorems are recorded and no open scaffolding is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.