prime_threehundredfiftynine
plain-language theorem explainer
The theorem asserts that the natural number 359 is prime. Number theorists applying Möbius or bigOmega functions in this module would cite it when verifying small squarefree inputs. The proof is a one-line term that invokes native_decide to evaluate the decidable primality predicate directly.
Claim. The natural number $359$ is prime, i.e., $359$ satisfies the predicate $Nat.Prime$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related predicates such as squarefreeness. Prime is the transparent alias for the standard predicate $Nat.Prime$ on natural numbers. Upstream results supply the interface classes and the basic Prime definition used here.
proof idea
The proof is a one-line term wrapper that applies native_decide to reduce the statement to a direct computational check of the Prime predicate on 359.
why it matters
This supplies a verified small-prime fact inside the arithmetic-functions scaffolding that supports Möbius footholds. It feeds the number-theory layer referenced by upstream interface classes for empirical programs and simplicial ledgers, though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.