mobius_eq_zero_of_not_squarefree
plain-language theorem explainer
If a natural number n is not squarefree then its Möbius function value vanishes. Number theorists applying Möbius inversion or Dirichlet convolution cite this property as a standard fact about the support of μ. The proof is a one-line wrapper that unfolds the local abbreviation for mobius and invokes the corresponding Mathlib result.
Claim. If $n$ is not squarefree, then $μ(n)=0$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ defined as the abbreviation mobius := ArithmeticFunction.moebius. Squarefree n means n is not divisible by any square greater than 1. The local setting is a collection of small footholds for later Dirichlet algebra and inversion formulas.
proof idea
The proof is a one-line wrapper that applies ArithmeticFunction.moebius_eq_zero_of_not_squarefree after rewriting with the definition of mobius.
why it matters
This theorem is invoked directly inside the proof of mobius_sq_eq_one_iff_squarefree, which states that μ(n)² = 1 if and only if n is squarefree. It supplies a basic arithmetic-function identity required for prime-counting arguments that appear in the Recognition Science number-theory layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.