vp_prime_ne
plain-language theorem explainer
Distinct primes p and q satisfy vp p q = 0, where vp extracts the exponent of the first argument in the factorization of the second. Number theorists constructing multiplicative functions or Möbius inversion over primes cite the result to dispatch the coprime case without further casework. The proof is a short term-mode reduction that converts the local Prime predicate to Nat.Prime via prime_iff, unfolds vp, rewrites with the standard factorization lemma, and simplifies using the given inequality.
Claim. For distinct primes $p, q$ in the natural numbers, the exponent of $p$ in the prime factorization of $q$ is zero: $v_p(q) = 0$.
background
The module supplies a thin wrapper over Mathlib's Nat.factorization. The function vp p n returns the exponent of p in the factorization of n. Prime is a transparent alias for Nat.Prime, and prime_iff equates the two predicates by reflexivity. The local goal is to furnish a small set of algebraic identities for vp that later files can reuse when treating squarefree numbers and Möbius functions.
proof idea
The term proof obtains a Mathlib Nat.Prime witness for q by applying the forward direction of prime_iff. It unfolds the definition of vp, rewrites the resulting factorization expression with the lemma that a prime's factorization is the singleton map sending the prime to 1, and finishes by simplifying with the symmetry of the supplied inequality p ≠ q.
why it matters
The theorem supplies the base case for distinct primes inside the factorization interface. Although the current dependency graph shows no direct users, the result supports the reusable identities vp_mul and vp_pow that the module documentation identifies as prerequisites for squarefree and Möbius constructions. It therefore forms part of the stable number-theoretic layer required by downstream Recognition Science arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.