vp_mul
plain-language theorem explainer
The vp function extracts the exponent of prime p in the factorization of n. Number theorists working with prime powers and factorization identities in Lean would cite vp_mul to reduce products to sums of exponents. The proof is a one-line simplification that unfolds the vp definition and applies the multiplicativity of the underlying factorization map.
Claim. Let $v_p(n)$ denote the exponent of prime $p$ in the prime factorization of natural number $n$. For $a,b$ nonzero natural numbers, $v_p(ab)=v_p(a)+v_p(b)$.
background
The Factorization module supplies a thin, stable wrapper around Mathlib's Nat.factorization. vp p n is defined as n.factorization p, returning the multiplicity of p in n. The upstream factorization_mul states that for nonzero a and b the factorization of a*b equals the sum of the individual factorizations, which is the key algebraic identity used here.
proof idea
One-line term proof that applies simp to unfold vp and substitute the result of factorization_mul.
why it matters
vp_mul supplies the additivity of the p-exponent under multiplication, a basic law required for later results such as vp_pow and for any work on squarefree numbers or Möbius functions in the primes module. It completes the small algebraic interface the module promises for downstream prime factorization arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.