prime_onehundredninetyone
plain-language theorem explainer
191 is a prime number. Number theorists building or verifying small cases inside arithmetic function libraries would cite this instance. The proof reduces the claim to a single native decision call that computes the absence of nontrivial divisors.
Claim. The natural number $191$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard primality predicate on natural numbers. The declaration supplies one concrete instance inside the primes section.
proof idea
One-line wrapper that applies the native_decide tactic to decide the primality statement by direct computation.
why it matters
It records a verified small-prime fact inside the arithmetic-functions file. No downstream uses are recorded yet, so the result remains a supporting verification point rather than a link in a larger chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.