vp_prime_pow
plain-language theorem explainer
The vp function returns the exponent of a given prime in the prime factorization of a natural number. This theorem asserts that the exponent of a prime p in p raised to k is exactly k whenever k is positive. It is invoked by lemmas that equate the valuation to k under the assumption that the number is a pure prime power. The short proof reduces the claim to the known factorization of powers and a direct ring computation.
Claim. If $p$ is prime and $k$ is a positive integer, then the exponent of $p$ in the prime factorization of $p^k$ equals $k$.
background
In this module a local valuation vp(p, n) is defined as the multiplicity of p in the prime factorization of n, implemented directly via Mathlib's Nat.factorization. The surrounding development supplies basic algebraic properties such as additivity under multiplication and compatibility with powers. The Prime predicate is the repository's transparent alias for Mathlib's Nat.Prime, with an equivalence theorem prime_iff that allows seamless transfer between the two.
proof idea
The argument first converts the hypothesis that p is Prime into the corresponding Mathlib Nat.Prime fact via prime_iff. It then unfolds the definition of vp, applies the theorem that factorization distributes over powers, substitutes the self-factorization of a prime, and concludes with a ring normalization.
why it matters
This identity is the key step used by vp_eq_of_eq_prime_pow to handle the general case in which an arbitrary n is assumed equal to p^k. The module as a whole supplies the algebraic laws needed for downstream prime-theoretic constructions such as squarefree predicates and Möbius functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.