Update Mathlib/Combinatorics/Enumerative/Pentagonal.lean

wwylele · bryangingechen · web-flow · commit d6d22447669a · 2026-04-29T09:29:44.000-04:00
Co-authored-by: Bryan Gin-ge Chen &lt;bryangingechen@gmail.com&gt;
diff --git a/Mathlib/Combinatorics/Enumerative/Pentagonal.lean b/Mathlib/Combinatorics/Enumerative/Pentagonal.lean
@@ -18,6 +18,7 @@ convention, but implicitly shows the monotonicity in `pentagonal_lt_pentagonal_n
 `pentagonal_neg_lt_pentagonal_add_one`.
 
 ## Main definitions
+
 * `pentagonal`: pentagonal numbers as a function `ℤ → ℕ`.
 
 ## TODO
