prime_onehundrednine
plain-language theorem explainer
109 is established as prime. Number theorists applying arithmetic functions such as the Möbius function to small primes would cite this fact when verifying inputs. The proof applies the native_decide tactic in one step to decide the statement from the definition of primality.
Claim. $109$ is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. Prime is introduced as a transparent alias for the standard primality predicate on natural numbers. This theorem supplies a concrete instance among the basic facts collected for later Dirichlet operations.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to confirm the primality predicate holds for 109.
why it matters
This supplies a verified small prime inside the arithmetic functions module. It supports direct evaluation of functions like Möbius on prime arguments. No downstream theorems are recorded, leaving open its eventual role in larger prime-based constructions within the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.