prime_seventythree
plain-language theorem explainer
73 is established as a prime natural number. Number theorists working with small primes inside arithmetic function wrappers would cite this for direct verification. The proof applies a computational decision procedure that checks the primality predicate without further lemmas.
Claim. The natural number 73 is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. Statements stay minimal until basic interfaces stabilize for Dirichlet algebra. The upstream definition supplies a repo-local alias for Mathlib's Nat.Prime kept transparent.
proof idea
A one-line wrapper applies the decide tactic to verify that 73 satisfies the primality predicate.
why it matters
This supplies a concrete primality fact inside the arithmetic functions module. It supports potential use in Möbius statements on primes, consistent with the module's role in number-theoretic scaffolding. No downstream theorems are recorded yet, leaving integration open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.