mobius_fifteen
plain-language theorem explainer
μ(15) equals 1 because 15 factors as the product of two distinct primes and is therefore squarefree. Number theorists applying Möbius inversion to divisor sums over 15 would cite this evaluation when expanding inclusion-exclusion terms. The proof reduces to a direct native computation of the arithmetic-function definition.
Claim. The Möbius function satisfies $μ(15) = 1$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function μ. The upstream definition states that mobius is the abbreviation for ArithmeticFunction.moebius, an arithmetic function ℕ → ℤ. By standard convention μ(n) equals (-1)^k when n is squarefree with k distinct prime factors and equals zero otherwise.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the Möbius function at 15 directly from its definition.
why it matters
This supplies a concrete value for μ at 15, a squarefree integer with two prime factors. It populates the arithmetic-functions module whose stated purpose is to stabilize basic interfaces before layering Dirichlet algebra. No downstream uses are recorded, so the declaration functions as a primitive foothold rather than a link in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.