vp_one
plain-language theorem explainer
The p-adic valuation of 1 equals zero for any natural number p. Number theorists building factorization identities would cite this when simplifying terms that contain the unit. The proof is a one-line simplification that unfolds the definition of the valuation.
Claim. $v_p(1) = 0$ for every natural number $p$.
background
The module supplies a thin wrapper over Mathlib's Nat.factorization to give a stable local valuation. The upstream definition states that vp p n is the exponent of p in the prime factorization of n (implemented as n.factorization p). This interface supports algebraic laws for multiplication and powers that later prime-number arguments rely on.
proof idea
The proof is a one-line wrapper that applies simp with the definition of vp.
why it matters
The identity anchors the valuation interface in the factorization module and supplies the base case needed for the multiplicative and power laws that follow. It therefore supports all downstream prime-factor work that the module was written to enable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.