prime_fourhundredninetyone
plain-language theorem explainer
491 is established as a prime number. Number theorists applying arithmetic functions such as the Möbius function in the Recognition Science setting would cite this fact for prime inputs. The proof is a term-mode native_decide that evaluates the primality predicate by direct computation.
Claim. $491$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is defined as a transparent alias for the standard predicate Nat.Prime on natural numbers. Upstream material includes the Prime alias from the Basic primes module together with several structure and class declarations from unrelated foundation and game-theory files that are pulled in by imports.
proof idea
The proof is a one-line term that applies native_decide to discharge the primality statement by compile-time evaluation of the decidable predicate.
why it matters
The declaration supplies a concrete prime instance inside the arithmetic-functions development. It can serve as input data for Möbius calculations or square-free checks once those interfaces are exercised. No downstream uses are recorded and the fact does not touch the forcing chain, RCL, or RS constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.