mobius_ne_zero_iff_squarefree
plain-language theorem explainer
The equivalence states that the Möbius function μ(n) is nonzero precisely when n is squarefree. Number theorists applying Möbius inversion or studying prime factorizations would cite this characterization. The proof is a one-line term wrapper that unfolds the local mobius abbreviation and invokes the matching Mathlib lemma.
Claim. For any natural number $n$, the Möbius function satisfies $μ(n) ≠ 0$ if and only if $n$ is squarefree.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The abbreviation mobius is defined as ArithmeticFunction.moebius, mapping natural numbers to integers. Squarefree n is the standard predicate that n is not divisible by p² for any prime p. This sits among sibling results on the Möbius function such as its definition and its values on primes.
proof idea
The proof is a one-line term wrapper. It applies simpa with the mobius abbreviation to reduce the local statement to ArithmeticFunction.moebius_ne_zero_iff_squarefree from Mathlib.
why it matters
This theorem supplies the positive direction for the vanishing criterion of the Möbius function and feeds directly into the sibling result mobius_eq_zero_iff_not_squarefree. It also supports the later bridge mobius_ne_zero_iff_vp_le_one that rewrites the condition in terms of prime exponents. The result provides a basic arithmetic foothold inside the NumberTheory.Primes layer without touching Recognition Science landmarks such as the J-function or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.