prime_dvd_of_dvd_pow
plain-language theorem explainer
If a prime divides a power of a natural number then it divides the base. Number theorists cite this when reducing divisibility statements that involve exponents. The proof is a one-line term that unfolds the local Prime alias via its equivalence and applies the standard Mathlib divisibility lemma for powers.
Claim. If $p$ is prime and $p$ divides $a^n$ for natural numbers $a,n$, then $p$ divides $a$.
background
The declaration sits in the Mathlib wrappers module whose purpose is to give stable, repo-local names for a small set of high-value prime theorems. This insulates downstream code from changes in Mathlib's API. Prime is the transparent alias abbrev Prime (n : ℕ) : Prop := Nat.Prime n. The companion theorem prime_iff states Prime n ↔ Nat.Prime n and is marked simp.
proof idea
One-line term proof that applies the left projection of prime_iff to hp, yielding Nat.Prime p, then feeds that fact together with the hypothesis h into Mathlib's dvd_of_dvd_pow lemma.
why it matters
It supplies a stable identifier for the basic prime-divisibility fact inside the NumberTheory.Primes submodule. The result supports sibling wrappers such as euclid_lemma and prime_dvd_mul_iff by providing a common building block for divisibility arguments. No direct link to the Recognition Science forcing chain or RCL exists, but the lemma belongs to the number-theoretic scaffolding required for the framework's algebraic constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.