prime_threehundredeightynine
plain-language theorem explainer
389 is established as a prime integer. Number theorists applying Möbius inversion or arithmetic functions to small primes would cite this fact. The proof is a direct computational decision that evaluates the primality predicate without manual factorization.
Claim. The positive integer 389 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 Nat.Prime predicate on natural numbers. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the primality predicate by direct computation.
why it matters
This supplies a concrete verified prime inside the arithmetic functions module. It supports potential downstream use of Möbius properties on small primes. No used_by edges are recorded, so the result currently stands as an isolated fact rather than feeding a larger chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.