squarefree_prime_dvd_iff_vp_eq_one
plain-language theorem explainer
For a nonzero squarefree natural number n and a prime p, p divides n if and only if the p-exponent vp(p,n) equals exactly 1. Number theorists working with squarefree integers and their prime factorizations cite this to translate divisibility into a precise valuation statement. The tactic proof splits the biconditional, invokes the squarefree exponent bound together with Mathlib factorization lemmas, and closes both directions with omega.
Claim. Let $n,p$ be natural numbers with $n$ nonzero, $n$ squarefree, and $p$ prime. Then $p$ divides $n$ if and only if the exponent of $p$ in the prime factorization of $n$ equals 1.
background
The Squarefree module links the standard Squarefree predicate on naturals to the repo-local valuation vp p n, defined as the exponent of p in n.factorization. The upstream theorem squarefree_iff_vp_le_one states that for nonzero n, Squarefree n holds precisely when vp p n is at most 1 for every prime p. Prime is the transparent alias for Nat.Prime, and prime_iff supplies the equivalence to the Mathlib predicate. This places the result inside the NumberTheory.Primes.Squarefree file, which assembles factorization identities for downstream use.
proof idea
The tactic proof first applies prime_iff to obtain Nat.Prime p. It constructs the biconditional. The forward direction uses factorization_pos_of_dvd to obtain a positive valuation from divisibility, combines it with the exponent bound from squarefree_iff_vp_le_one, and concludes equality to 1 via omega. The reverse direction applies pow_dvd_iff_le_factorization to recover p^1 divides n from the valuation hypothesis, again closing with omega.
why it matters
The result directly supports the companion theorem squarefree_prime_not_dvd_iff_vp_eq_zero that handles the complementary non-divisibility case. It supplies a basic equivalence in the vp-based characterization of squarefree numbers inside the NumberTheory.Primes layer. These factorization tools underpin later arguments that rely on clean control of prime exponents, consistent with the Recognition Science emphasis on precise counting in the phi-ladder and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.