squarefree_iff_vp_le_one_of_prime
plain-language theorem explainer
A nonzero natural number n is squarefree precisely when the p-adic valuation vp(p,n) is at most 1 for every prime p. Number theorists using valuation-based tests for squarefreeness cite this to restrict checks to primes. The tactic proof splits the biconditional, reduces both directions to the unrestricted squarefree_iff_vp_le_one via primality case analysis, and discharges the non-prime case with the zero valuation property.
Claim. For nonzero natural number $n$, $n$ is square-free if and only if $v_p(n) ≤ 1$ for every prime $p$.
background
The module links the standard squarefree predicate on naturals to the valuation vp p n, defined as the exponent of p in the prime factorization of n. Squarefree means no squared prime divides n, which is equivalent to all exponents being 0 or 1. This prime-restricted form specializes the general characterization, relying on the sibling result that gives the bound for all natural numbers p.
proof idea
Tactic proof opens with constructor to split the biconditional. Forward direction invokes the unrestricted squarefree_iff_vp_le_one to obtain the bound for all p then restricts to primes. Reverse direction assumes the prime bound, performs by_cases on whether p is prime, applies the hypothesis when it is, and for non-primes rewrites vp to zero via the factorization rule before applying zero_le.
why it matters
Supplies the prime-only variant of the squarefree characterization inside the NumberTheory.Primes.Squarefree module. It supports arithmetic lemmas on factorization that feed into broader Recognition Science constructions such as forcing chains and self-reference structures, even though no immediate downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.