prime_dvd_mul_iff
plain-language theorem explainer
Euclid's lemma in biconditional form states that a prime p divides a times b exactly when p divides a or p divides b. Number theorists working inside the Recognition Science number-theory layer cite this for all factorization steps that follow from primality. The proof is a one-line term wrapper that invokes the Mathlib divisibility lemma after a simplification pass that unfolds the local Prime abbreviation.
Claim. If $p$ is prime then $p$ divides $a$ times $b$ if and only if $p$ divides $a$ or $p$ divides $b$.
background
The declaration lives in the Mathlib-wrappers module whose purpose is to give repo-local names to a small set of high-value prime theorems so that downstream code never depends directly on Mathlib API changes. Prime is the transparent abbreviation for the standard natural-number primality predicate. The only substantive upstream dependency is the basic Prime alias together with the Mathlib statement that a prime divides a product precisely when it divides one of the factors.
proof idea
The proof is a one-line term wrapper. It calls Nat.Prime.dvd_mul on the three arguments and the primality hypothesis, then uses simpa with the local Prime abbreviation to discharge the goal.
why it matters
The biconditional supplies the logical direction needed by the sibling implication form euclid_lemma in the same file. The wrapper module exists precisely so that all later prime-divisibility arguments inside NumberTheory.Primes can cite stable local identifiers. In the Recognition framework this supports the prime-factor steps that appear in mass-ladder constructions and in any argument that extracts unique factorization from the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.