typo in L05le_mul_right.lean

This commit is contained in:
Yannick Seurin
2024-06-14 11:47:56 +02:00
committed by GitHub
parent 08b488b32b
commit 9bc59952a8

View File

@@ -19,7 +19,7 @@ TheoremDoc MyNat.le_mul_right as "le_mul_right" in "≤"
Introduction
"
In Prime Number World we will be proving that $2$ is prime.
To do this, we will have to rule out things like $2 37 × 42.$
To do this, we will have to rule out things like $2 = 37 × 42.$
We will do this by proving that any factor of $2$ is at most $2$,
which we will do using this lemma. The proof I have in mind manipulates the hypothesis
until it becomes the goal, using pretty much everything which we've proved in this world so far.