Proof of `Every number greater than 1 has a prime divisor`

groundedproofs/Lax242665Proofs/PrimeDivisor.lean · lax-242665

What this proof establishes

no assumptions

lem✓Lax242665.PrimeDivisor

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

In the paper

page 2 of this submission's paper

Description

The least divisor of $n$ greater than $1$ is prime and divides $n$ .