pow_dvd_iff_le_vp
plain-language theorem explainer
The equivalence asserts that for a prime p and nonzero natural number n, p^k divides n precisely when k does not exceed the exponent of p in the factorization of n. Number theorists building divisibility arguments over the local prime interface would cite this when moving between power divisibility and valuation bounds. The proof is a term-mode wrapper that converts the local Prime hypothesis via prime_iff and hands the problem to Mathlib's factorization lemma.
Claim. Let $p$ be prime and let $n$ be a nonzero natural number. Then $p^k$ divides $n$ if and only if $k$ is at most the exponent of $p$ in the prime factorization of $n$.
background
The module supplies a thin stable interface over Mathlib's Nat.factorization. The function vp p n extracts the exponent of p in the factorization of n. Prime is the transparent alias for Nat.Prime, and prime_iff equates the two so that Mathlib lemmas become available without extra hypotheses.
proof idea
The term proof first obtains a Nat.Prime witness from the local Prime hypothesis by applying prime_iff. It then simplifies the definition of vp and invokes the Mathlib lemma pow_dvd_iff_le_factorization on the resulting Nat.Prime and the nonzero assumption.
why it matters
The result supplies the standard divisibility-to-exponent link inside the factorization module. It is used directly by the theorem that equates prime divisibility with positive valuation, thereby supporting the algebraic laws required for squarefree and Möbius constructions downstream in the primes layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.