repunit_index_nineteen
plain-language theorem explainer
19 is established as prime to index the repunit R_19. Number theorists examining repunit properties or arithmetic foundations would reference this verified fact. Native decision procedure confirms the result directly at compile time.
Claim. $19$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime facts support repunit indexing components. The local Prime abbreviation is defined as an alias for Nat.Prime.
proof idea
The proof is a one-line term that invokes native_decide to verify primality of 19.
why it matters
This supplies a basic prime index for repunit R_19 inside the arithmetic functions module. It contributes verified number-theoretic facts that may feed Recognition Science constructions involving primes. No downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.