prime_dvd_iff_gcd_eq
plain-language theorem explainer
A prime p divides a natural number n precisely when their gcd equals p. Number theorists maintaining the Recognition monolith cite this wrapper to keep prime divisibility statements independent of Mathlib API shifts. The short proof first converts the local Prime predicate to the standard Nat.Prime via the equivalence lemma, then applies the two standard gcd identities in each direction.
Claim. Let $p$ be a prime number and $n$ a natural number. Then $p$ divides $n$ if and only if the greatest common divisor of $p$ and $n$ equals $p$.
background
The module supplies stable, repo-local names for prime theorems from Mathlib so that downstream code depends only on IndisputableMonolith.NumberTheory.Primes names. Prime is the transparent alias for Nat.Prime. The upstream Primes definition collects all primes as the set {n | Nat.Prime n}, and prime_iff supplies the equivalence Prime n ↔ Nat.Prime n.
proof idea
The proof obtains Nat.Prime p from the hypothesis via prime_iff, then splits the biconditional. One direction uses the fact that if p divides n then gcd(p,n)=p; the converse rewrites the gcd assumption and invokes that gcd(p,n) divides n.
why it matters
This wrapper belongs to the prime toolkit that supports number-theoretic arguments throughout the monolith. It fills the role of a basic divisibility criterion without exposing Mathlib internals. No direct link to the forcing chain or RCL appears here; it remains a supporting lemma for prime factorization steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.