forked from leanprover-community/mathlib4
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathWanted.lean
More file actions
20 lines (19 loc) · 1 KB
/
Copy pathWanted.lean
File metadata and controls
20 lines (19 loc) · 1 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
module -- shake: keep-all --deprecated_module: ignore
public import Wanted.Analysis.Convex.Cone.Basic
public import Wanted.Analysis.Real.Pi.Chudnovsky
public import Wanted.CategoryTheory.Limits.Shapes.Countable
public import Wanted.Combinatorics.SimpleGraph.StronglyRegular
public import Wanted.Computability.TuringMachine.Computable
public import Wanted.Data.EReal.Operations
public import Wanted.Geometry.Euclidean.Volume.Measure
public import Wanted.Geometry.Manifold.PoincareConjecture
public import Wanted.Geometry.Manifold.SmoothEmbedding
public import Wanted.GroupTheory.GroupAction.Jordan
public import Wanted.Order.KrullDimension
public import Wanted.Probability.Combinatorics.BinomialRandomGraph.Defs
public import Wanted.Probability.Distributions.Binomial
public import Wanted.RingTheory.Congruence.Basic
public import Wanted.RingTheory.Etale.Descent
public import Wanted.RingTheory.KrullDimension.Basic
public import Wanted.RingTheory.SimpleModule.Basic
public import Wanted.RingTheory.SimpleModule.WedderburnArtin