prime_eq_of_dvd_pow
plain-language theorem explainer
If p and q are primes and p divides q to the power m, then p equals q. Number theorists maintaining the Recognition Science prime toolkit cite this for divisor arguments inside prime-power expressions. The proof is a one-line term wrapper that converts the local Prime predicate to Nat.Prime via prime_iff and delegates to the Mathlib primitive Nat.prime_eq_prime_of_dvd_pow.
Claim. Let $p,q$ be prime natural numbers and $m$ a natural number. If $p$ divides $q^m$, then $p=q$.
background
The declaration sits inside the Mathlib wrappers module for prime theorems. That module supplies stable repo-local names so downstream code can depend on IndisputableMonolith identifiers without chasing upstream API changes. The local Prime predicate and its equivalence prime_iff are imported from the sibling Basic module.
proof idea
The proof is a one-line wrapper. It applies prime_iff to hp and hq to obtain Nat.Prime instances, then passes those together with the divisibility hypothesis h to Nat.prime_eq_prime_of_dvd_pow.
why it matters
This result completes the prime-power divisor toolkit inside NumberTheory.Primes.Wrappers. It supplies a stable interface for factorization steps that appear in ledger factorization, spectral emergence, and phi-forcing structures. The wrapper pattern ensures that changes in Mathlib's prime API remain isolated from the Recognition Science forcing chain and J-cost calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.