prime_sixtyone
plain-language theorem explainer
The declaration asserts that 61 satisfies the primality predicate on natural numbers. Number theorists using arithmetic functions such as the Möbius function would cite this fact when verifying squarefreeness or related properties for small primes. The proof consists of a single decide tactic that discharges the decidable primality check.
Claim. $61$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. The local setting keeps statements minimal so that deeper Dirichlet algebra and inversion can be added once basic interfaces stabilize. The upstream result defines Prime as a transparent alias for the standard primality predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the decidable proposition that 61 is prime.
why it matters
This fact supports basic checks inside the arithmetic functions module for primes that appear in Möbius calculations. It occupies a slot in the NumberTheory.Primes hierarchy but records no downstream uses. No direct tie to the Recognition Science forcing chain or constants appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.