vp_mul
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not apply when a=0 or b=0.
- Restricted to natural numbers.
- Does not require p to be prime.
- Does not compute explicit numerical values.
formal statement (Lean)
37theorem vp_mul (p a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) :
38 vp p (a * b) = vp p a + vp p b := by
proof body
Term-mode proof.
39 simp [vp, Nat.factorization_mul ha hb]
40
41/-- The `vp` exponent scales under powers: `vp p (n^k) = k * vp p n`. -/