Skip to content

Commit

Permalink
C05/S02: fix typo
Browse files Browse the repository at this point in the history
  • Loading branch information
@mtoohey31 @avigad
mtoohey31 authored and avigad committed May 27, 2024
1 parent f8b9278 commit b36fbc2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -269,7 +269,7 @@ both follow the same canonical order. Simplifying with these
rules, and the corresponding rules for addition, is a handy trick.
Returning to summation identities, we suggest stepping through the following proof
that the sum of the natural numbers up to an including :math:`n` is
that the sum of the natural numbers up to and including :math:`n` is
:math:`n (n + 1) / 2`.
The first step of the proof clears the denominator.
This is generally useful when formalizing identities,
Expand Down

0 comments on commit b36fbc2

Please sign in to comment.