chore(*): minor import cleanup (#3546)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Jul 25, 2020 · 0379d3a · 0379d3a
1 parent 2a456a9
commit 0379d3a
Show file tree

Hide file tree

Showing 8 changed files with 7 additions and 11 deletions.
diff --git a/src/algebra/group/pi.lean b/src/algebra/group/pi.lean
@@ -3,7 +3,8 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
-import algebra.ordered_group tactic.pi_instances
+import algebra.ordered_group
+import tactic.pi_instances
 /-!
 # Pi instances for groups and monoids
 

diff --git a/src/algebra/ring/pi.lean b/src/algebra/ring/pi.lean
@@ -3,7 +3,9 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
-import tactic.pi_instances algebra.group.pi algebra.ring.basic
+import tactic.pi_instances
+import algebra.group.pi
+import algebra.ring.basic
 
 /-!
 # Pi instances for ring

diff --git a/src/category_theory/endomorphism.lean b/src/category_theory/endomorphism.lean
@@ -5,7 +5,6 @@ Authors: Yury Kudryashov, Scott Morrison, Simon Hudon
 
 Definition and basic properties of endomorphisms and automorphisms of an object in a category.
 -/
-import category_theory.category
 import category_theory.groupoid
 import data.equiv.mul_add
 

diff --git a/src/category_theory/groupoid.lean b/src/category_theory/groupoid.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Reid Barton All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton, Scott Morrison, David Wärn
 -/
-import category_theory.category
 import category_theory.epi_mono
 
 namespace category_theory

diff --git a/src/data/equiv/encodable/lattice.lean b/src/data/equiv/encodable/lattice.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Floris van Doorn
 -/
 import data.equiv.encodable.basic
-import data.finset
+import data.finset.basic
 import data.set.disjointed
 /-!
 # Lattice operations on encodable types

diff --git a/src/data/indicator_function.lean b/src/data/indicator_function.lean
@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou
 -/
 import algebra.group.pi
-import algebra.module.basic
-import data.set.disjointed
+import group_theory.group_action
 import data.support
 import data.finset.lattice
 

diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean
@@ -7,7 +7,6 @@ Nonnegative real numbers.
 -/
 import algebra.linear_ordered_comm_group_with_zero
 import algebra.big_operators.ring
-import data.finset.lattice
 import data.real.basic
 import data.indicator_function
 

diff --git a/src/topology/algebra/monoid.lean b/src/topology/algebra/monoid.lean
@@ -5,11 +5,8 @@ Authors: Johannes Hölzl, Mario Carneiro
 
 Theory of topological monoids.
 -/
-
 import topology.continuous_on
-import algebra.group.pi
 import group_theory.submonoid.basic
-import algebra.group.prod
 import deprecated.submonoid
 
 open classical set filter topological_space