Skip to content

Commit

Permalink
Correct minor informal math typo in S03_Infinitely_Many_Primes.lean
Browse files Browse the repository at this point in the history
  • Loading branch information
benjaminfjones authored and avigad committed Sep 8, 2024
1 parent 398dbcb commit dda3bb6
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ One way to formulate this is as the statement that
for every natural number
:math:`n`, there is a prime number greater than :math:`n`.
To prove this, let :math:`p` be any prime factor of :math:`n! + 1`.
If :math:`p` is less than :math:`n`, it divides :math:`n!`.
If :math:`p` is less than or equal to :math:`n`, it divides :math:`n!`.
Since it also divides :math:`n! + 1`, it divides 1, a contradiction.
Hence :math:`p` is greater than :math:`n`.
Expand Down

0 comments on commit dda3bb6

Please sign in to comment.