coprime_comm_iff_not_dvd_of_prime
plain-language theorem explainer
Symmetric coprimality for primes states that a natural number n shares no common factors with a prime p exactly when p fails to divide n. Researchers building number-theoretic tools inside Recognition Science cite this when manipulating divisibility in prime-based arguments. The proof reduces immediately to the non-symmetric form via a single rewrite of the coprimality relation.
Claim. Let $p$ be a prime and $n$ a natural number. Then $n$ is coprime to $p$ if and only if $p$ does not divide $n$.
background
The module supplies stable aliases for Mathlib prime results to insulate downstream code from API changes. Prime is the repo-local name for the predicate that a natural number is prime. The upstream result coprime_iff_not_dvd_of_prime asserts the non-commutative version: gcd(p,n)=1 iff p does not divide n.
proof idea
The proof is a one-line wrapper. It rewrites the goal using the commutativity of the coprimality predicate and then applies the base theorem coprime_iff_not_dvd_of_prime.
why it matters
This declaration supplies the symmetric form of the coprimality criterion for primes, completing the toolkit started by its non-commutative sibling. It supports stable references in prime factorization arguments within the Recognition Science number theory layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.