mobius_thirty
plain-language theorem explainer
The declaration computes the Möbius function value at 30 as -1. Number theorists applying inclusion-exclusion or Dirichlet series would cite this evaluation for the factorization 30 = 2·3·5. The proof is a one-line native decision that evaluates the arithmetic function definition directly.
Claim. $μ(30) = -1$, where $μ$ is the Möbius function on the positive integers.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, starting with the Möbius function $μ$ as a map from natural numbers to integers. The upstream abbrev identifies this map with ArithmeticFunction.moebius. The local setting keeps statements minimal so that Dirichlet algebra and inversion can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line term that applies native_decide to evaluate the Möbius function at 30 from its definition.
why it matters
This supplies a concrete value for $μ$ at a square-free integer with three distinct prime factors. It supports arithmetic-function calculations inside the NumberTheory.Primes module. No parent theorem or Recognition Science chain step is referenced in the supplied results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.