squarefree_iff_vp_le_one
plain-language theorem explainer
A nonzero natural number n is squarefree precisely when every prime exponent in its factorization is at most one. Number theorists working with the Möbius function or arithmetic functions cite this equivalence to translate between the global Squarefree predicate and the local valuation vp. The proof is a one-line term wrapper that applies Mathlib's Nat.squarefree_iff_factorization_le_one after unfolding vp.
Claim. For nonzero $n$, $n$ is squarefree if and only if $v_p(n) ≤ 1$ for every natural number $p$.
background
The module connects the standard Squarefree predicate on naturals to the repo-local valuation vp p n, which returns the exponent of p in n.factorization. This rests on the imported factorization tools and the alias Prime for Nat.Prime. The local theoretical setting is to support arithmetic-function proofs that need to switch between global squarefreeness and per-prime exponents.
proof idea
Term-mode one-liner: simpa [vp] using Nat.squarefree_iff_factorization_le_one (n := n) hn. The tactic unfolds the definition of vp and hands the goal directly to the Mathlib theorem.
why it matters
This equivalence is the parent for mobius_ne_zero_iff_vp_le_one and the three sibling squarefree lemmas (dichotomy, prime-divisibility, and prime-restricted form). It supplies the number-theoretic bridge required by downstream arithmetic results in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.