We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent f788039 commit e70ce7cCopy full SHA for e70ce7c
1 file changed
Mathlib/Combinatorics/Enumerative/PentagonalNumbers.lean
@@ -3,11 +3,13 @@ Copyright (c) 2025 Beibei Xiong. All rights reserved.
3
Released under Apache 2.0 license as described in the file LICENSE.
4
Authors: Beibei Xiong
5
-/
6
-import Mathlib.Algebra.Order.Ring.Star
7
-import Mathlib.Analysis.Normed.Ring.Lemmas
8
-import Mathlib.Combinatorics.Enumerative.Partition
9
-import Mathlib.Data.Int.Star
10
-import Mathlib.RingTheory.PowerSeries.Basic
+module
+
+public import Mathlib.Algebra.Order.Ring.Star
+public import Mathlib.Analysis.Normed.Ring.Lemmas
+public import Mathlib.Combinatorics.Enumerative.Partition
11
+public import Mathlib.Data.Int.Star
12
+public import Mathlib.RingTheory.PowerSeries.Basic
13
14
/-!
15
# Pentagonal numbers, parity of strict partitions, and a finite product cut-off
0 commit comments