mobius_eq_zero_iff_not_squarefree
plain-language theorem explainer
The Möbius function vanishes on a natural number precisely when that number fails to be squarefree. Number theorists applying inclusion-exclusion or inverting the zeta function would invoke the equivalence to restrict summation domains. The argument is a one-line term proof that negates the companion non-vanishing criterion via congruence of negations and simplification.
Claim. For every natural number $n$, the Möbius function satisfies $μ(n)=0$ if and only if $n$ is not squarefree.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function defined as the arithmetic function moebius. The companion theorem states that μ(n) is nonzero exactly when n is squarefree. This equivalence is obtained by logical negation of that statement. The local setting is arithmetic functions providing Möbius footholds for later Dirichlet algebra once basic interfaces stabilize.
proof idea
The term proof applies not_congr to the companion theorem mobius_ne_zero_iff_squarefree and then simplifies the resulting negation with not_ne_iff.
why it matters
This result completes the basic characterization of the Möbius function within the arithmetic functions module. It supports later squarefree detection inside the Recognition Science number-theoretic scaffolding, although no downstream uses are recorded yet. It supplies the missing half of the squarefree criterion needed for multiplicative-function control.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.