prime_sixhundredsixtyone
plain-language theorem explainer
661 is established as a prime integer. Researchers applying arithmetic functions such as the Möbius function to specific primes in the Recognition Science number theory development would cite this result. The proof is a direct invocation of Lean's native decision procedure for primality.
Claim. The integer $661$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repository-local alias for the standard Nat.Prime predicate on natural numbers. Upstream results include the Prime abbrev together with is predicates from foundation modules that certify collision-free or tautological properties.
proof idea
The proof is a one-line term that applies native_decide to verify the primality of 661.
why it matters
This fact supplies a concrete prime instance for Möbius evaluations inside the ArithmeticFunctions module. It populates the NumberTheory.Primes hierarchy that supports later Dirichlet algebra layers referenced in the module documentation. No downstream uses are recorded and no direct link to the forcing chain or RCL appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.