vp_prime_self
plain-language theorem explainer
The result states that the exponent of a prime p in its own factorization equals one. Number theorists using the local valuation interface for prime factorization work would cite this identity as the base case. The proof converts the hypothesis via the prime equivalence and simplifies the definition against the self-factorization property.
Claim. Let $p$ be a prime natural number. Then the exponent of $p$ in the prime factorization of $p$ equals one.
background
The module supplies a thin wrapper around Mathlib's Nat.factorization. The function vp p n extracts the exponent of p in the factorization of n. The predicate Prime is the transparent alias for Nat.Prime, linked by the equivalence prime_iff that identifies the two notions directly.
proof idea
The proof applies prime_iff to obtain Nat.Prime p from the hypothesis. It then rewrites via simp on the definition of vp together with the Mathlib fact that a prime factors to itself with exponent one.
why it matters
This identity supplies the self-case inside the factorization interface of the NumberTheory.Primes.Factorization module. It anchors the reusable laws vp_mul and vp_pow that later support squarefree detection and Möbius inversion steps in the Recognition pipeline. No open questions remain attached to this base fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.