chore(*): remove default.lean files that had nothing but imports (#18408

)
leanprover-community · Feb 9, 2023 · 916aaa1 · 916aaa1
1 parent 639b66d
commit 916aaa1
Show file tree

Hide file tree

Showing 60 changed files with 6 additions and 266 deletions.
diff --git a/archive/100-theorems-list/82_cubing_a_cube.lean b/archive/100-theorems-list/82_cubing_a_cube.lean
@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 -/
 import data.real.basic
 import data.set.finite
-import data.set.intervals
+import data.set.intervals.disjoint
 
 /-!
 Proof that a cube (in dimension n ≥ 3) cannot be cubed:

diff --git a/docs/tutorial/category_theory/Ab.lean b/docs/tutorial/category_theory/Ab.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import algebra.category.Group
+import algebra.category.Group.abelian
 import category_theory.limits.shapes.kernels
 
 noncomputable theory

diff --git a/docs/tutorial/category_theory/calculating_colimits_in_Top.lean b/docs/tutorial/category_theory/calculating_colimits_in_Top.lean
@@ -1,5 +1,4 @@
 import topology.category.Top.limits
-import category_theory.limits.shapes
 import topology.instances.real
 import topology.tactic
 

diff --git a/src/algebra/big_operators/default.lean b/src/algebra/big_operators/default.lean
diff --git a/src/algebra/category/Group/default.lean b/src/algebra/category/Group/default.lean
diff --git a/src/algebra/category/Mon/default.lean b/src/algebra/category/Mon/default.lean
diff --git a/src/algebra/category/Ring/default.lean b/src/algebra/category/Ring/default.lean
diff --git a/src/algebra/char_p/default.lean b/src/algebra/char_p/default.lean
diff --git a/src/algebra/continued_fractions/computation/default.lean b/src/algebra/continued_fractions/computation/default.lean
diff --git a/src/algebra/continued_fractions/default.lean b/src/algebra/continued_fractions/default.lean
diff --git a/src/algebra/default.lean b/src/algebra/default.lean
diff --git a/src/algebra/group/default.lean b/src/algebra/group/default.lean
diff --git a/src/algebra/group_power/default.lean b/src/algebra/group_power/default.lean
diff --git a/src/algebra/group_with_zero/default.lean b/src/algebra/group_with_zero/default.lean
diff --git a/src/algebra/module/default.lean b/src/algebra/module/default.lean
diff --git a/src/algebra/ring/default.lean b/src/algebra/ring/default.lean
diff --git a/src/category_theory/adjunction/default.lean b/src/category_theory/adjunction/default.lean
diff --git a/src/category_theory/concrete_category/default.lean b/src/category_theory/concrete_category/default.lean
diff --git a/src/category_theory/functor/default.lean b/src/category_theory/functor/default.lean
diff --git a/src/category_theory/limits/shapes/default.lean b/src/category_theory/limits/shapes/default.lean
diff --git a/src/category_theory/monad/default.lean b/src/category_theory/monad/default.lean
diff --git a/src/category_theory/products/default.lean b/src/category_theory/products/default.lean
diff --git a/src/category_theory/subobject/default.lean b/src/category_theory/subobject/default.lean
diff --git a/src/category_theory/sums/default.lean b/src/category_theory/sums/default.lean
diff --git a/src/control/traversable/default.lean b/src/control/traversable/default.lean
diff --git a/src/data/fin/tuple/default.lean b/src/data/fin/tuple/default.lean
diff --git a/src/data/finite/default.lean b/src/data/finite/default.lean
diff --git a/src/data/finset/default.lean b/src/data/finset/default.lean
diff --git a/src/data/finsupp/default.lean b/src/data/finsupp/default.lean
diff --git a/src/data/list/default.lean b/src/data/list/default.lean
diff --git a/src/data/multiset/default.lean b/src/data/multiset/default.lean
diff --git a/src/data/mv_polynomial/default.lean b/src/data/mv_polynomial/default.lean
diff --git a/src/data/nat/choose/default.lean b/src/data/nat/choose/default.lean
diff --git a/src/data/pfunctor/univariate/default.lean b/src/data/pfunctor/univariate/default.lean
diff --git a/src/data/polynomial/default.lean b/src/data/polynomial/default.lean
diff --git a/src/data/polynomial/degree/default.lean b/src/data/polynomial/degree/default.lean
diff --git a/src/data/qpf/multivariate/default.lean b/src/data/qpf/multivariate/default.lean
diff --git a/src/data/rat/default.lean b/src/data/rat/default.lean
diff --git a/src/data/rbtree/default.lean b/src/data/rbtree/default.lean
diff --git a/src/data/set/default.lean b/src/data/set/default.lean
diff --git a/src/data/set/intervals/default.lean b/src/data/set/intervals/default.lean
diff --git a/src/data/sigma/default.lean b/src/data/sigma/default.lean
diff --git a/src/field_theory/minpoly/default.lean b/src/field_theory/minpoly/default.lean
diff --git a/src/geometry/euclidean/default.lean b/src/geometry/euclidean/default.lean
diff --git a/src/group_theory/group_action/default.lean b/src/group_theory/group_action/default.lean
diff --git a/src/group_theory/submonoid/default.lean b/src/group_theory/submonoid/default.lean
diff --git a/src/linear_algebra/clifford_algebra/default.lean b/src/linear_algebra/clifford_algebra/default.lean
diff --git a/src/linear_algebra/default.lean b/src/linear_algebra/default.lean
diff --git a/src/linear_algebra/matrix/default.lean b/src/linear_algebra/matrix/default.lean
diff --git a/src/number_theory/padics/default.lean b/src/number_theory/padics/default.lean
diff --git a/src/order/default.lean b/src/order/default.lean
diff --git a/src/order/filter/default.lean b/src/order/filter/default.lean
diff --git a/src/ring_theory/adjoin/default.lean b/src/ring_theory/adjoin/default.lean
diff --git a/src/ring_theory/polynomial/default.lean b/src/ring_theory/polynomial/default.lean
diff --git a/src/topology/category/Top/default.lean b/src/topology/category/Top/default.lean
diff --git a/test/delta_instance.lean b/test/delta_instance.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
 -/
-import data.set
+import data.set.basic
 import algebra.category.Mon.basic
 
 def X : Type := set ℕ

diff --git a/test/free_algebra.lean b/test/free_algebra.lean
@@ -5,7 +5,7 @@ Authors: Eric Wieser
 -/
 
 import linear_algebra.exterior_algebra.basic
-import linear_algebra.clifford_algebra
+import linear_algebra.clifford_algebra.basic
 
 /-!
 Tests that the ring instances for `free_algebra` and derived quotient types actually work.

diff --git a/test/library_search/ring_theory.lean b/test/library_search/ring_theory.lean
@@ -5,7 +5,7 @@ Authors: Scott Morrison
 -/
 import tactic.suggest
 import ring_theory.principal_ideal_domain
-import ring_theory.polynomial
+import ring_theory.polynomial.basic
 
 open_locale polynomial
 /- Turn off trace messages so they don't pollute the test build: -/

diff --git a/test/localized/localized.lean b/test/localized/localized.lean
@@ -1,5 +1,5 @@
 import tactic.localized
-import algebra.group_power
+import algebra.group_power.lemmas
 
 open tactic
 local infix ` ⊹ `:59 := nat.mul

diff --git a/test/mk_iff_of_inductive.lean b/test/mk_iff_of_inductive.lean
@@ -1,4 +1,3 @@
-import data.list
 import data.list.perm
 import data.multiset.basic