prime_sixhundrednineteen
plain-language theorem explainer
619 is established as a prime number. Number theorists working with arithmetic functions such as the Möbius function would cite this fact for small-prime cases in inversion formulas or prime-power sums. The proof is a one-line term that invokes native decision to confirm the property directly.
Claim. The integer $619$ 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 natural-number primality predicate. This supplies a concrete primality instance usable in Möbius or big-Omega calculations within the file.
proof idea
The proof is a one-line term wrapper that applies native_decide to discharge the primality claim for 619.
why it matters
The result supplies a basic primality fact inside the arithmetic-functions module. It supports any downstream prime-dependent arithmetic identities, though the current dependency graph lists no immediate parent theorems or uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.