Skip to content

Commit 2b2261e

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

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
@@ -14,7 +14,7 @@ This file introduces (generalized) pentagonal numbers $k(3k-1)/2$ for integer $k
1414
1515
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
17-
convention, but implicitly shows the monotonicity by `pentagonal_lt_pentagonal_neg` and
17+
convention, but implicitly shows the monotonicity in `pentagonal_lt_pentagonal_neg` and
1818
`pentagonal_neg_lt_pentagonal_add_one`.
1919
2020
## Main definitions

0 commit comments

Comments
 (0)