Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Primality claims restated from lax-242665` (1st statement)

groundedproofs/Lax771644Proofs/ExternalPrimes.lean · lax-771644

What this proof establishes

thm✓Lax771644.ExternalPrimes (1st statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Restates the prime-divisor claim of An Introduction to Lax.

Proof strategy

Apply Lax242665.PrimeDivisor.existsprimedvdLax242665.PrimeDivisor.exists_prime_dvd; the two statements have the same type.

Attribution

The mathematics belongs to lax−242665lax-242665; this submission only re-exports it so that the benchmark drawing contains an external assumption node.