mobius_prime
plain-language theorem explainer
The theorem records that the Möbius function evaluates to negative one at every prime. Number theorists applying Möbius inversion or square-free decompositions would cite this evaluation. The argument converts the local Prime predicate to Mathlib's Nat.Prime via an equivalence lemma and invokes the standard arithmetic-function case for primes.
Claim. If $p$ is a prime natural number, then the Möbius function satisfies $μ(p) = -1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The abbrev mobius identifies ArithmeticFunction.moebius as the map from natural numbers to integers. The abbrev Prime is the transparent alias for Nat.Prime. The upstream prime_iff equivalence converts between the repository predicate and Mathlib's native version. The local setting keeps statements minimal so that Dirichlet inversion can be added once interfaces stabilize.
proof idea
Term-mode proof. The first step obtains a Nat.Prime witness from the hypothesis via prime_iff. The second step applies ArithmeticFunction.moebius_apply_prime and uses simpa with the mobius abbreviation to finish.
why it matters
The result supplies the prime case of the Möbius function inside the ArithmeticFunctions module. It forms part of the basic footholds for later square-free and inversion work in the NumberTheory.Primes hierarchy. No downstream uses are recorded; the declaration therefore sits at the base of the arithmetic-function scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.