mobius_ne_zero_iff_vp_le_one
plain-language theorem explainer
The equivalence asserts that for nonzero n the Möbius function μ(n) is nonzero precisely when every prime valuation v_p(n) is at most one. Number theorists applying Möbius inversion or inclusion-exclusion would cite this characterization to translate between arithmetic-function and factorization language. The proof is a one-line wrapper that composes the already-established mobius non-zero iff squarefree equivalence with the squarefree iff vp ≤ 1 equivalence.
Claim. For $n ∈ ℕ$ with $n ≠ 0$, the Möbius function satisfies μ(n) ≠ 0 if and only if the p-adic valuation v_p(n) ≤ 1 for every prime p.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ (an abbrev for ArithmeticFunction.moebius). A sibling result states that μ(n) ≠ 0 exactly when n is square-free. The valuation function vp extracts the exponent of a given prime in the factorization of n, and square-freeness is defined by the condition that all such exponents are at most one. The local theoretical setting is arithmetic functions as footholds for later Dirichlet algebra and inversion, kept deliberately lightweight.
proof idea
The term proof opens with constructor to split the biconditional. The forward direction invokes mobius_ne_zero_iff_squarefree to obtain square-freeness from nonzero μ, then applies squarefree_iff_vp_le_one to reach the valuation bound. The reverse direction runs the same two equivalences in the opposite order, first recovering square-freeness from the valuation hypothesis and then nonzero μ from square-freeness.
why it matters
This result supplies a direct translation between the Möbius function and prime-exponent data inside the NumberTheory layer. It sits downstream of the core mobius definition and the square-free characterization, providing a convenient interface for any later arithmetic work that may feed into Recognition Science structures such as the phi-ladder or J-cost calculations. No immediate parent theorems or open questions in the T0-T8 chain are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.