Skip to content

Commit 599592e

Browse files
Update Mathlib/Combinatorics/Enumerative/Pentagonal.lean
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
1 parent f56677c commit 599592e

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Combinatorics/Enumerative/Pentagonal.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ public import Mathlib.Data.Int.SuccPred
1212
1313
This file introduces (generalized) pentagonal numbers $k(3k-1)/2$ for integer $k$.
1414
15-
Some source, such as A001318 in the OEIS, orders generalized pentagonal numbers by indices
15+
Some sources, such as A001318 in the OEIS, order generalized pentagonal numbers by indices
1616
$k = 0, 1, -1, 2, -2, \cdots$ to form a strictly monotone sequence. This file doesn't follow this
1717
convention, but implicitly shows the monotonicity by `pentagonal_lt_pentagonal_neg` and
1818
`pentagonal_neg_lt_pentagonal_add_one`.

0 commit comments

Comments
 (0)