We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 1105a82 commit 7d96bc2Copy full SHA for 7d96bc2
1 file changed
Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean
@@ -5,10 +5,10 @@ Authors: Chris Birkbeck
5
-/
6
module
7
8
-import Mathlib.Data.Nat.ModEq
+public import Mathlib.Data.Nat.ModEq
9
public import Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
10
public import Mathlib.NumberTheory.ModularForms.Discriminant
11
-import Mathlib.RingTheory.PowerSeries.Order
+public import Mathlib.RingTheory.PowerSeries.Order
12
13
import Mathlib.Algebra.Order.Floor.Semifield
14
0 commit comments