coprime_iff_not_dvd_of_prime
plain-language theorem explainer
A prime p is coprime to n precisely when p does not divide n. Number theorists maintaining the Recognition monolith cite this wrapper to shield downstream code from Mathlib API shifts. The proof is a one-line term that casts the local Prime hypothesis to Nat.Prime via prime_iff and delegates to the standard coprimality criterion.
Claim. For all natural numbers $p$ and $n$, if $p$ is prime then $p$ and $n$ are coprime if and only if $p$ does not divide $n$.
background
The module supplies stable repo-local names for high-value prime theorems already present in Mathlib. Prime is the transparent alias abbrev Prime (n : ℕ) : Prop := Nat.Prime n. The upstream theorem prime_iff states Prime n ↔ Nat.Prime n for any natural n, allowing the local hypothesis to be converted without new content.
proof idea
The term first obtains Nat.Prime p from hp : Prime p by applying prime_iff, then invokes the Mathlib lemma coprime_iff_not_dvd on that instance.
why it matters
This result is invoked by the symmetric wrapper coprime_comm_iff_not_dvd_of_prime in the same file. It belongs to the prime toolkit whose purpose is to keep downstream code dependent on IndisputableMonolith.NumberTheory.Primes names rather than direct Mathlib imports. No direct tie to the T0-T8 forcing chain or Recognition Composition Law appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.