mobius_thirtyfive
plain-language theorem explainer
μ(35) equals 1 because 35 factors as 5 times 7 and is squarefree with exactly two distinct primes. Analytic number theorists cite this explicit evaluation when checking small cases in Möbius inversion or Dirichlet convolution. The proof reduces to a single native decision step that evaluates the arithmetic function definition directly.
Claim. The Möbius function satisfies $μ(35) = 1$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function μ defined as an arithmetic function from naturals to integers. The upstream definition identifies mobius as the standard Möbius function ArithmeticFunction.moebius. This specific theorem records the value at 35, which factors as 5 times 7 and is squarefree with two distinct prime factors.
proof idea
The proof is a one-line wrapper that invokes native_decide to compute the value of the Möbius function at 35 from its definition.
why it matters
This value contributes to the collection of explicit Möbius evaluations in the arithmetic functions module, supporting downstream calculations in number theory such as inclusion-exclusion or Dirichlet convolution. It aligns with the general property that μ(n) equals (-1)^k for squarefree n with k prime factors. No immediate parent theorems are listed, but it populates the basic interface for the Möbius function in the Recognition Science number theory layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.