Lax Lean Archive

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

Proof of `Primality claims restated from lax-242665` (2nd statement)

groundedproofs/Lax771644Proofs/ExternalPrimes.lean · lax-771644

What this proof establishes

thm✓Lax771644.ExternalPrimes (2nd 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 infinitude-of-primes claim of An Introduction to Lax.

Proof strategy

Apply Lax242665.InfinitelyManyPrimes.existsprimegtLax242665.InfinitelyManyPrimes.exists_prime_gt; 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.