prime_onehundredfortynine
plain-language theorem explainer
149 is a prime number. Number theorists applying arithmetic functions such as the Möbius function to concrete cases would cite this fact when checking square-freeness or inversion formulas involving 149. The proof is a single native_decide tactic that reduces the claim to a decidable computational check.
Claim. $149$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard predicate Nat.Prime on natural numbers. This supplies a concrete instance of that predicate for the integer 149.
proof idea
One-line wrapper that applies the native_decide tactic to discharge the primality statement by direct computation.
why it matters
The declaration supplies a basic prime fact usable in arithmetic-function calculations within the module. No downstream uses are recorded yet. It fits the module's stated goal of keeping statements lightweight before layering deeper Dirichlet algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.