prime_onehundredthirteen
plain-language theorem explainer
Establishes that 113 is prime in the natural numbers. Number theorists using arithmetic functions or explicit prime checks in larger identities would cite it as a verified base case. The proof is a single native decision tactic that computes primality directly.
Claim. The natural number 113 is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. Prime is the transparent alias for Nat.Prime. This theorem sits in the primes submodule alongside Möbius and bigOmega definitions, providing concrete facts for the arithmetic interface.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the primality predicate.
why it matters
It supplies a verified prime fact supporting the arithmetic functions layer. No downstream theorems reference it yet, but it aligns with the need for explicit primes when building Möbius-based identities or squarefree checks. In the Recognition framework it provides basic number-theoretic scaffolding without touching forcing chains or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.