mobius_six
plain-language theorem explainer
The Möbius function evaluates to 1 at 6, consistent with the rule that μ(n) equals (-1)^k when n is squarefree with k distinct prime factors. Number theorists applying Möbius inversion to sums over divisors or inclusion-exclusion identities reference this concrete value. The proof is a one-line native decision that evaluates the arithmetic function definition at the given input.
Claim. $μ(6) = 1$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ spelled as an arithmetic function from naturals to integers. The upstream abbrev establishes mobius as the standard ArithmeticFunction.moebius, keeping statements minimal to support later Dirichlet algebra and inversion layers. This local setting treats μ as the standard inclusion-exclusion tool whose values are determined by the prime factorization of the argument.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the Möbius function at 6.
why it matters
This supplies a concrete evaluation of μ at 6 that serves as a basic foothold for arithmetic function calculations inside the NumberTheory.Primes module. It aligns with the squarefree characterization where μ(n) = (-1)^k for k distinct primes and supports general inversion formulas. No downstream uses are recorded, leaving it as an isolated reference value rather than a step in a larger chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.