prime_sixhundredseventyseven
plain-language theorem explainer
677 is asserted to be prime. Researchers working with the arithmetic functions module would cite it to anchor small-prime base cases for Möbius function evaluations and squarefree checks. The proof is a one-line native_decide wrapper that delegates primality verification to the kernel's computational checker.
Claim. The natural number $677$ is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Prime is the repo-local alias for Nat.Prime. Upstream results supply collision-free and tautological structures from foundation and game-theory modules, though this declaration relies only on the Prime abbreviation and the native decision procedure.
proof idea
The proof is a one-line wrapper that applies native_decide to the primality predicate on 677.
why it matters
This supplies a verified small-prime fact inside the arithmetic-functions scaffolding that supports Möbius inversion and Dirichlet algebra in the Recognition framework. It fills a concrete base case required by sibling declarations such as mobius_prime and mobius_apply_of_squarefree. No direct link to the T0-T8 forcing chain or phi-ladder appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.