mobius_twentyone
plain-language theorem explainer
Evaluation of the Möbius function yields μ(21) = 1. Number theorists applying inclusion-exclusion or Dirichlet inversion cite such concrete cases for verification during computations. The proof reduces to a single native decision step that evaluates the arithmetic function definition outright.
Claim. $μ(21) = 1$, where 21 is square-free with exactly two distinct prime factors.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ (aliased as ArithmeticFunction.moebius). This function maps natural numbers to integers and vanishes on inputs with repeated prime factors while returning (-1)^k on square-free inputs with k distinct primes. The upstream abbrev mobius simply re-exports the standard Mathlib definition as an ArithmeticFunction ℤ.
proof idea
The proof is a one-line term wrapper that applies native_decide to compute the value of mobius at 21 directly from its definition.
why it matters
This supplies a basic concrete evaluation inside the arithmetic-functions module, confirming the sign for the two-prime square-free case. It serves as a foothold for any later Dirichlet-algebra or inversion work that may be layered on top, consistent with the module's stated goal of stabilizing basic interfaces before deeper results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.