euclid_lemma
plain-language theorem explainer
Euclid's lemma asserts that if a prime p divides the product a times b then p divides a or p divides b. Number theorists building the Recognition Science prime toolkit cite this wrapper to keep stable local names for classical divisibility facts. The proof is a one-line term that projects the left direction from the sibling prime_dvd_mul_iff equivalence.
Claim. Let $p$ be prime. If $p$ divides $a b$ then $p$ divides $a$ or $p$ divides $b$.
background
The module supplies repo-local aliases for a small set of high-value prime theorems already present in Mathlib so that downstream code can depend on stable IndisputableMonolith names rather than chasing upstream API shifts. Prime is the transparent abbreviation for Nat.Prime. The local setting is therefore purely notational scaffolding; no new mathematical content is introduced here.
proof idea
The proof is a one-line term wrapper that applies prime_dvd_mul_iff to the hypotheses hp and h and then selects the first component of the resulting equivalence.
why it matters
This wrapper anchors the classical Euclid lemma inside the Recognition Science number-theory layer. It supplies a fixed reference point for the sibling results on prime divisibility of powers that appear later in the same file. No downstream uses are recorded yet, but the declaration closes a direct dependency on the underlying Mathlib equivalence while preserving the implication form required by later combinatorial arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.