prime_threehundredseventynine
plain-language theorem explainer
379 is a prime number. Researchers applying arithmetic functions such as the Möbius function in the Recognition Science number theory layer would cite this fact for prime arguments. The proof is a one-line term wrapper that invokes Lean's native decision procedure to settle the primality check.
Claim. The natural number $379$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting keeps statements minimal until Dirichlet inversion layers stabilize. Prime is a transparent alias for Nat.Prime. Upstream results supply structural definitions from foundation modules (collision-free classes, algebraic tautologies, and mechanism design structures) and the Ramanujan bridge, though none are invoked in the primality check itself.
proof idea
The proof is a term-mode one-line wrapper that applies native_decide to reduce the statement directly to a native Lean computation of primality.
why it matters
This supplies a verified prime constant for arithmetic function applications in the NumberTheory.Primes module. It fills a basic foothold ahead of Möbius or squarefree evaluations, consistent with the framework's use of concrete number-theoretic facts. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.