prime_sixhundredseven
plain-language theorem explainer
607 is asserted to be a prime natural number. Number theorists working with explicit arithmetic functions or small-prime cases in Möbius inversion would reference this fact during concrete calculations. The verification is a direct computational check via native decision procedures.
Claim. $607$ is a prime number.
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 predicate Nat.Prime on natural numbers. Upstream results include the abbreviation Prime (n : ℕ) := Nat.Prime n together with structural hypotheses ensuring algebraic consistency across foundation modules.
proof idea
The proof is a one-line term that invokes native_decide to computationally verify the primality predicate on 607.
why it matters
This supplies an explicit prime fact inside the arithmetic-functions module. It supports downstream handling of square-free integers and Möbius values at primes, though no direct used-by edges are recorded. The declaration fills a basic number-theoretic placeholder required for any RS-native prime ladder or mass-formula checks that reference small integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.