-
Notifications
You must be signed in to change notification settings - Fork 2
/
Modformsported.lean
34 lines (34 loc) · 1.86 KB
/
Modformsported.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
import Modformsported.ForMathlib.AuxpLemmas
import Modformsported.ForMathlib.Cotangent.CotangentIdentity
import Modformsported.ForMathlib.Cotangent.basic
import Modformsported.ForMathlib.DependencyExtractor
import Modformsported.ForMathlib.EisensteinSeries.Basic2
import Modformsported.ForMathlib.EisensteinSeries.ModularForm
import Modformsported.ForMathlib.EisensteinSeries.SL2lemmas
import Modformsported.ForMathlib.EisensteinSeries.basic
import Modformsported.ForMathlib.EisensteinSeries.bounded_at_infty
import Modformsported.ForMathlib.EisensteinSeries.boundingfunctions
import Modformsported.ForMathlib.EisensteinSeries.bounds
import Modformsported.ForMathlib.EisensteinSeries.generalLevels
import Modformsported.ForMathlib.EisensteinSeries.genlevlbounded
import Modformsported.ForMathlib.EisensteinSeries.lattice_functions
import Modformsported.ForMathlib.EisensteinSeries.mdifferentiable
import Modformsported.ForMathlib.EisensteinSeries.partial_sum_tendsto_uniformly
import Modformsported.ForMathlib.EisensteinSeries.q_expansions
import Modformsported.ForMathlib.EisensteinSeries.summable
import Modformsported.ForMathlib.ExpSummableLemmas
import Modformsported.ForMathlib.LogDeriv
import Modformsported.ForMathlib.ModForms2
import Modformsported.ForMathlib.QExpAux
import Modformsported.ForMathlib.TsumLemmas
import Modformsported.ModForms.DiscriminantForm
import Modformsported.ModForms.GeneralQExpansions.CuspformBound
import Modformsported.ModForms.GeneralQExpansions.QExpansion
import Modformsported.ModForms.HolomorphicFunctions
import Modformsported.ModForms.ModularGroup.MatM
import Modformsported.ModForms.ModularGroup.ModGroup
import Modformsported.ModForms.ModularGroup.ModularGroup
import Modformsported.ModForms.ModularityConjecture
import Modformsported.ModForms.Riemzeta
import Modformsported.ModForms.UnformLimitsOfHolomorphic
import Modformsported.ModForms.WeierstrassMTest