chore(*): removing unneeded imports (#9278)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/analysis/asymptotics/asymptotic_equivalent.lean

@@ -12,7 +12,7 @@ import analysis.normed_space.ordered
 In this file, we define the relation `is_equivalent u v l`, which means that `u-v` is little o of
 `v` along the filter `l`.
 
-Unlike `is_[oO]` relations, this one requires `u` and `v` to have the same codomaine `β`. While the
+Unlike `is_[oO]` relations, this one requires `u` and `v` to have the same codomain `β`. While the
 definition only requires `β` to be a `normed_group`, most interesting properties require it to be a
 `normed_field`.
 

src/analysis/calculus/fderiv_measurable.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel, Yury Kudryashov
 -/
 import analysis.calculus.deriv
 import measure_theory.constructions.borel_space
+import tactic.ring_exp
 
 /-!
 # Derivative is measurable

src/analysis/calculus/inverse.lean

@@ -7,6 +7,7 @@ import analysis.calculus.times_cont_diff
 import analysis.normed_space.banach
 import topology.local_homeomorph
 import topology.metric_space.contracting
+import tactic.ring_exp
 
 /-!
 # Inverse function theorem

src/analysis/normed_space/basic.lean

@@ -11,8 +11,6 @@ import topology.instances.ennreal
 import topology.metric_space.algebra
 import topology.metric_space.completion
 import topology.sequences
-import topology.locally_constant.algebra
-import topology.continuous_function.algebra
 
 /-!
 # Normed spaces
@@ -2042,7 +2040,7 @@ end summable
 
 section cauchy_product
 
-/-! ## Multipliying two infinite sums in a normed ring
+/-! ## Multiplying two infinite sums in a normed ring
 
 In this section, we prove various results about `(∑' x : ι, f x) * (∑' y : ι', g y)` in a normed
 ring. There are similar results proven in `topology/algebra/infinite_sum` (e.g `tsum_mul_tsum`),
@@ -2127,7 +2125,7 @@ begin
   ... ≤ ∑ kl in antidiagonal n, ∥f kl.1∥ * ∥g kl.2∥ : sum_le_sum (λ i _, norm_mul_le _ _)
 end
 
-/-- The Cauchy product formula for the product of two infinites sums indexed by `ℕ`,
+/-- The Cauchy product formula for the product of two infinite sums indexed by `ℕ`,
     expressed by summing on `finset.nat.antidiagonal`.
     See also `tsum_mul_tsum_eq_tsum_sum_antidiagonal` if `f` and `g` are
     *not* absolutely summable. -/
@@ -2145,7 +2143,7 @@ begin
   exact summable_norm_sum_mul_antidiagonal_of_summable_norm hf hg
 end
 
-/-- The Cauchy product formula for the product of two infinites sums indexed by `ℕ`,
+/-- The Cauchy product formula for the product of two infinite sums indexed by `ℕ`,
     expressed by summing on `finset.range`.
     See also `tsum_mul_tsum_eq_tsum_sum_range` if `f` and `g` are
     *not* absolutely summable. -/
@@ -2189,38 +2187,3 @@ instance [semi_normed_group V] : normed_group (completion V) :=
 
 end completion
 end uniform_space
-
-namespace locally_constant
-
-variables {X Y : Type*} [topological_space X] [topological_space Y] (f : locally_constant X Y)
-
-/-- The inclusion of locally-constant functions into continuous functions as a multiplicative
-monoid hom. -/
-@[to_additive "The inclusion of locally-constant functions into continuous functions as an
-additive monoid hom.", simps]
-def to_continuous_map_monoid_hom [monoid Y] [has_continuous_mul Y] :
-  locally_constant X Y →* C(X, Y) :=
-{ to_fun    := coe,
-  map_one' := by { ext, simp, },
-  map_mul'  := λ x y, by { ext, simp, }, }
-
-/-- The inclusion of locally-constant functions into continuous functions as a linear map. -/
-@[simps] def to_continuous_map_linear_map (R : Type*) [semiring R] [topological_space R]
-  [add_comm_monoid Y] [module R Y] [has_continuous_add Y] [has_continuous_smul R Y] :
-  locally_constant X Y →ₗ[R] C(X, Y) :=
-{ to_fun    := coe,
-  map_add'  := λ x y, by { ext, simp, },
-  map_smul' := λ x y, by { ext, simp, }, }
-
-/-- The inclusion of locally-constant functions into continuous functions as an algebra map. -/
-@[simps] def to_continuous_map_alg_hom (R : Type*) [comm_semiring R] [topological_space R]
-  [semiring Y] [algebra R Y] [topological_ring Y] [has_continuous_smul R Y] :
-  locally_constant X Y →ₐ[R] C(X, Y) :=
-{ to_fun    := coe,
-  map_one'  := by { ext, simp, },
-  map_mul'  := λ x y, by { ext, simp, },
-  map_zero' := by { ext, simp, },
-  map_add'  := λ x y, by { ext, simp, },
-  commutes' := λ r, by { ext x, simp [algebra.smul_def], }, }
-
-end locally_constant

src/category_theory/adjunction/basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton, Johan Commelin, Bhavik Mehta
 -/
 import category_theory.equivalence
-import data.equiv.basic
 
 namespace category_theory
 open category

src/category_theory/limits/preserves/shapes/terminal.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import category_theory.limits.preserves.limits
-import category_theory.limits.shapes
+import category_theory.limits.shapes.terminal
 
 /-!
 # Preserving terminal object

src/category_theory/preadditive/projective.lean

@@ -5,6 +5,7 @@ Authors: Markus Himmel, Scott Morrison
 -/
 import algebra.homology.exact
 import category_theory.types
+import category_theory.limits.shapes.biproducts
 
 /-!
 # Projective objects and categories with enough projectives

src/category_theory/sites/types.lean

@@ -5,7 +5,6 @@ Authors: Kenny Lau
 -/
 
 import category_theory.sites.canonical
-import category_theory.sites.sheaf_of_types
 
 /-!
 # Grothendieck Topology and Sheaves on the Category of Types

src/category_theory/subobject/factor_thru.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Scott Morrison
 -/
 import category_theory.subobject.basic
+import category_theory.preadditive
 
 /-!
 # Factoring through subobjects

src/category_theory/subobject/mono_over.lean

@@ -5,6 +5,7 @@ Authors: Bhavik Mehta, Scott Morrison
 -/
 import category_theory.currying
 import category_theory.limits.over
+import category_theory.limits.shapes.images
 import category_theory.adjunction.reflective
 
 /-!

src/category_theory/triangulated/pretriangulated.lean

@@ -6,7 +6,6 @@ Authors: Luke Kershaw
 import category_theory.additive.basic
 import category_theory.shift
 import category_theory.preadditive.additive_functor
-import category_theory.triangulated.basic
 import category_theory.triangulated.rotate
 
 /-!

src/linear_algebra/clifford_algebra/equivs.lean

@@ -5,7 +5,6 @@ Authors: Eric Wieser
 -/
 import algebra.quaternion_basis
 import data.complex.module
-import linear_algebra.clifford_algebra.basic
 import linear_algebra.clifford_algebra.conjugation
 
 /-!

src/linear_algebra/finite_dimensional.lean

@@ -5,8 +5,6 @@ Authors: Chris Hughes
 -/
 import algebra.algebra.subalgebra
 import field_theory.finiteness
-import linear_algebra.dimension
-import ring_theory.principal_ideal_domain
 
 /-!
 # Finite dimensional vector spaces

src/ring_theory/localization.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston
 -/
-
+import tactic.ring_exp
 import data.equiv.ring
 import group_theory.monoid_localization
 import ring_theory.ideal.operations

src/ring_theory/polynomial/basic.lean

@@ -7,7 +7,6 @@ Authors: Kenny Lau
 import algebra.char_p.basic
 import data.mv_polynomial.comm_ring
 import data.mv_polynomial.equiv
-import data.polynomial.field_division
 import ring_theory.principal_ideal_domain
 import ring_theory.polynomial.content
 

src/ring_theory/polynomial/content.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 import algebra.gcd_monoid.finset
-import data.polynomial
+import data.polynomial.field_division
 import data.polynomial.erase_lead
 import data.polynomial.cancel_leads
 

src/topology/continuous_function/locally_constant.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2021 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import topology.locally_constant.algebra
+import topology.continuous_function.basic
+
+/-!
+# The algebra morphism from locally constant functions to continuous functions.
+
+-/
+
+namespace locally_constant
+
+variables {X Y : Type*} [topological_space X] [topological_space Y] (f : locally_constant X Y)
+
+/-- The inclusion of locally-constant functions into continuous functions as a multiplicative
+monoid hom. -/
+@[to_additive "The inclusion of locally-constant functions into continuous functions as an
+additive monoid hom.", simps]
+def to_continuous_map_monoid_hom [monoid Y] [has_continuous_mul Y] :
+  locally_constant X Y →* C(X, Y) :=
+{ to_fun    := coe,
+  map_one' := by { ext, simp, },
+  map_mul'  := λ x y, by { ext, simp, }, }
+
+/-- The inclusion of locally-constant functions into continuous functions as a linear map. -/
+@[simps] def to_continuous_map_linear_map (R : Type*) [semiring R] [topological_space R]
+  [add_comm_monoid Y] [module R Y] [has_continuous_add Y] [has_continuous_smul R Y] :
+  locally_constant X Y →ₗ[R] C(X, Y) :=
+{ to_fun    := coe,
+  map_add'  := λ x y, by { ext, simp, },
+  map_smul' := λ x y, by { ext, simp, }, }
+
+/-- The inclusion of locally-constant functions into continuous functions as an algebra map. -/
+@[simps] def to_continuous_map_alg_hom (R : Type*) [comm_semiring R] [topological_space R]
+  [semiring Y] [algebra R Y] [topological_ring Y] [has_continuous_smul R Y] :
+  locally_constant X Y →ₐ[R] C(X, Y) :=
+{ to_fun    := coe,
+  map_one'  := by { ext, simp, },
+  map_mul'  := λ x y, by { ext, simp, },
+  map_zero' := by { ext, simp, },
+  map_add'  := λ x y, by { ext, simp, },
+  commutes' := λ r, by { ext x, simp [algebra.smul_def], }, }
+
+end locally_constant