prime_onehundredone
plain-language theorem explainer
The declaration establishes that 101 is a prime natural number. Number theorists working with arithmetic functions would cite it as a concrete base case when evaluating Möbius values or divisor counts on small inputs. The proof is a direct one-line native_decide tactic that evaluates the primality predicate at compile time.
Claim. $101$ is a prime number, i.e., the predicate Prime$(101)$ holds where Prime$(n)$ is the standard definition that $n$ has no divisors other than 1 and itself.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and its basic properties. A dedicated section collects small primes from 101 to 199 to support concrete calculations. The sole upstream dependency is the transparent alias Prime$(n) :=$ Nat.Prime$(n)$, which imports the standard primality predicate without additional hypotheses.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic directly to the primality statement for 101.
why it matters
This supplies a verified small prime instance inside the arithmetic-functions module, serving as a base case for later Möbius and divisor identities. It does not connect to the Recognition Science forcing chain, phi-ladder, or constants such as alpha or G.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.